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