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