defpred S1[ 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 S1[A] )
from SUBSET_1:sch 3();
hence
ex b1 being Subset-Family of R st
for A being Subset of R holds
( A in b1 iff ex a being Element of R st A = Class a )
; verum