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