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