set(auto2).

formulas(sos).
% axioms for theorem 6

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))))))).

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 x all y ((Object(x) & Object(y)) -> (PartPH(x,y) <-> (exists F (Property(F) & IsTheFormOf(y,F) & Enc(x,F))))).

all x all G ((Object(x) & Property(G)) -> (IsTheFormOf(x,G) <-> (IsAFormOf(x,G)  & (all y (IsAFormOf(y,G) -> y=x))))). 

% theorem 
-(all F all y all z ((Property(F) & Object(y) & Object(z) & Enc(y,F) & Enc(z,F) & y!=z) -> (exists x (IsTheFormOf(x,F) & PartPH(y,x) & PartPH(z,x))))).
end_of_list.