thus ex X being set st
for e being object holds
( e in X iff ( e in WFF & S₁[e] ) ) from XBOOLE_0:sch 1(); :: thesis: verum