let X be Subset of REAL; :: thesis: ( X is closed iff X = Cl X )

hereby :: thesis: ( X = Cl X implies X is closed )

set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
assume X is closed ; :: thesis: X = Cl X
then X in { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
then A1: Cl X c= X by SETFAM_1:3;
X c= Cl X by Th58;
hence X = Cl X by A1; :: thesis: verum

end;

thus ( X = Cl X implies X is closed ) ; :: thesis: verum