set(auto2). formulas(sos). % axioms for theorem 1a (existence) all x all G ((Object(x) & Property(G)) -> (IsAFormOf(x,G) <-> Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F)))))). all G (Property(G) -> (exists x (Object(x) & Ex1(A,x,W) & (all F (Property(F)-> (Enc(x,F) <-> Implies(G,F))))))). % theorem 1a -(all G (Property(G) -> (exists x (Object(x) & IsAFormOf(x,G))))). end_of_list.