formulas(sos). % axioms for theorem 14b Proposition(L). all x all p (Object(x)&Proposition(p)-> (Encp(x,p)<-> (exists F (Property(F)&F=VAC(p)&Enc(x,F))))). 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 p all x (Object(x)&Proposition(p)-> (TrueIn(p,x)<->Encp(x,p))). all x (Object(x)-> (Maximal2(x)<->Situation(x)& (all p (Proposition(p)->TrueIn(p,x))))). all x (Object(x)-> (Partial2(x)<-> -Maximal2(x))). exists x (Object(x)&Ex1At(A,x,W)& (all F (Property(F)-> (Enc(x,F)<->F!=F)))). end_of_list.