set(auto2). formulas(sos). % axioms for theorem 2 all F all G ((Property(F) & Property(G)) -> (Implies(F,G) <-> (all x all w (Point(w) -> (Ex1(F,x,w) -> Ex1(G,x,w)))))). 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 x all G ((Object(x) & Property(G)) -> (IsTheFormOf(x,G) <-> (IsAFormOf(x,G) & (all y (IsAFormOf(y,G) -> y=x))))). % theorem 2 -(all x all G ((Object(x) & Property(G)) -> (IsTheFormOf(x,G) -> Enc(x,G)))). end_of_list.