formulas(sos).
% axioms for theorem 6
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.

