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

reconsider H = { h where h is Subset of X : S_{1}[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

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

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