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