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