let X be Subset of REAL ; :: thesis: for Y being closed Subset of REAL st X c= Y holds
Cl X c= Y
let Y be closed Subset of REAL ; :: thesis: ( X c= Y implies Cl X c= Y )
assume A1: X c= Y ; :: thesis: Cl X c= Y
set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ;
Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } by A1;
hence Cl X c= Y by SETFAM_1:4; :: thesis: verum