defpred S₁[ set ] means ex W being Subset of T st
( $1 = Cl W & W in FX );
thus ex S being Subset-Family of T st
for Z being Subset of T holds
( Z in S iff S₁[Z] ) from SUBSET_1:sch 3(); :: thesis: verum