let X be RealNormSpace; :: thesis: for Z being Subset of X holds Z c= Cl Z

let Z be Subset of X; :: thesis: Z c= Cl Z

reconsider W = Z as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

Cl Z = Cl W by EQCL1;

hence Z c= Cl Z by PRE_TOPC:18; :: thesis: verum

let Z be Subset of X; :: thesis: Z c= Cl Z

reconsider W = Z as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;

Cl Z = Cl W by EQCL1;

hence Z c= Cl Z by PRE_TOPC:18; :: thesis: verum