let X, Y be Subset of REAL ; :: thesis: ( X c= Y implies Cl X c= Cl Y )
assume A1: X c= Y ; :: thesis: Cl X c= Cl Y
Y c= Cl Y by Th33;
then A2: X c= Cl Y by A1, XBOOLE_1:1;
set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
Cl Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } by A2;
hence Cl X c= Cl Y by SETFAM_1:4; :: thesis: verum