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