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