let X be RealNormSpace; :: thesis: for Y being Subset of X
for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds
Cl Y = Cl Z
let Y be Subset of X; :: thesis: for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds
Cl Y = Cl Z
let Z be Subset of (LinearTopSpaceNorm X); :: thesis: ( Y = Z implies Cl Y = Cl Z )
assume A1: Y = Z ; :: thesis: Cl Y = Cl Z
ex Z0 being Subset of (LinearTopSpaceNorm X) st
( Z0 = Y & Cl Y = Cl Z0 ) by defcl;
hence Cl Y = Cl Z by A1; :: thesis: verum