op(300,prefix,~).

formulas(sos).
% axioms for theorem 10
Point(W).

all p (Proposition(p)->Proposition(~p)).

all w all p (Point(w)&Proposition(p)-> (True(~p,w)<-> -True(p,w))).

all x (Object(x)-> (Actual(x)<-> (Situation(x) & (all p (Proposition(p)-> (TrueIn(p,x)->True(p,W))))))).

all x (Actual(x) -> Object(x)).

end_of_list.