defpred S_{1}[ 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_{1}[P] )
from SUBSET_1:sch 3(); :: thesis: verum

thus ex G being Subset-Family of D st

for P being Subset of D holds

( P in G iff S