defpred S_{1}[ set ] means $1 c= f . $1;

reconsider H = { h where h is Subset of X : S_{1}[h] } as Subset-Family of X from DOMAIN_1:sch 7();

union H is Subset of X ;

hence union { h where h is Subset of X : h c= f . h } is Subset of X ; :: thesis: verum

reconsider H = { h where h is Subset of X : S

union H is Subset of X ;

hence union { h where h is Subset of X : h c= f . h } is Subset of X ; :: thesis: verum