defpred S₁[ set ] means ex u being Element of Q. I st $1 = QClass. u;
thus ex S being Subset-Family of (Q. I) st
for A being Subset of (Q. I) holds
( A in S iff S₁[A] ) from SUBSET_1:sch 3(); :: thesis: verum