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