op(300,prefix,~).

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

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

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

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.