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