defpred S₁[ set ] means ex a being Element of R st $1 = Class a;
ex F being Subset-Family of R st
for A being Subset of R holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of R st
for A being Subset of R holds
( A in b₁ iff ex a being Element of R st A = Class a ) ; :: thesis: verum