defpred S₁[ set ] means f . $1 c= $1;
reconsider H = { h where h is Subset of X : S₁[h] } as Subset-Family of X from DOMAIN_1:sch 7();
reconsider H = H as Subset-Family of X ;
meet H is Subset of X ;
hence meet { h where h is Subset of X : f . h c= h } is Subset of X ; :: thesis: verum