formulas(usable). all x all F ((Object(x) & Property(F)) -> ((exists d (Point(d) & EncAt(x,F,d))) -> (all d (Point(d) -> EncAt(x,F,d))))). all x all p all d ((Object(x) & Proposition(p) & Point(d)) -> (EncpAt(x,p,d) <-> (exists F (Property(F) & F=VAC(p) & EncAt(x,F,d))))). end_of_list.