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.