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