set(auto2).

formulas(sos).
% axioms for theorem 4
all x all y ((Object(x) & Object(y)) -> (PartPH(x,y) <-> (exists F (Property(F) & IsTheFormOf(y,F) & Enc(x,F))))).

% theorem 4
-(all x all y all G ((Object(x) & Object(y) & Property(G)) -> (IsTheFormOf(x,G) -> (Enc(y,G) -> PartPH(y,x))))).
end_of_list.
