defpred S₁[ Subset of ] means $1 ` in F;
thus ex G being Subset-Family of D st
for P being Subset of holds
( P in G iff S₁[P] ) from SUBSET_1:sch 3(); :: thesis: verum