defpred S1[ set ] means ex b being Element of B st b c= $1;
ex Z being Subset-Family of X st
for x being Subset of X holds
( x in Z iff S1[x] )
from SUBSET_1:sch 3();
hence
ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex b being Element of B st b c= x )
; verum