formulas(sos).
% axioms for theorem 11
Proposition(L).

-True(L,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.