defpred S₁[ set ] means $1 c= f . $1;
reconsider H = { h where h is Subset of X : S₁[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