defpred S1[ Subset of ] means ( X c= $1 & $1 is closed );
reconsider Z = { A where A is Subset of : S1[A] } as Subset-Family of from DOMAIN_1:sch 7();
reconsider Z = Z as Subset-Family of ;
meet Z is Subset of
;
hence
meet { A where A is Subset of : ( X c= A & A is closed ) } is Subset of
; verum