formulas(sos). % axioms for theorem 5 all x (Situation(x) -> Object(x)). all x (Object(x) -> (Situation(x) <-> Ex1At(A,x,W) & (all F (Property(F)-> (Enc(x,F) -> (exists p (Proposition(p) & F=VAC(p)))))))). all x all y (Object(x) & Object(y)-> (PartOf(x,y) <-> Ex1At(A,x,W) & Ex1At(A,y,W) & (all F (Property(F) -> (Enc(x,F) -> Enc(y,F)))))). all x all y (Ex1At(A,x,W) & Ex1At(A,y,W) -> ((all F (Property(F) -> (Enc(x,F) <-> Enc(y,F)))) -> x=y)). end_of_list.