defpred S₁[ Subset of REAL] means ( X c= X & X 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 ;
Z is closed

proof

let Y be Subset of REAL; :: according to MEASURE6:def 7 :: thesis: ( Y in Z implies Y is closed )
assume Y in Z ; :: thesis: Y is closed
then ex A being Subset of REAL st
( Y = A & X c= A & A is closed ) ;
hence Y is closed ; :: thesis: verum

end;

hence Cl X is closed by Th56; :: thesis: verum