defpred S₁[ set ] means ex Y being Subset-Family of X st
( Y c= A & $1 = union Y );
ex Z being Subset-Family of X st
for x being Subset of X holds
( x in Z iff S₁[x] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset-Family of X st
for x being Subset of X holds
( x in b₁ iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ; :: thesis: verum