defpred S1[ set ] means ex Y being Subset-Family of X st
( Y c= A & Y is finite & $1 = Intersect Y );
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 Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) )
; verum