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

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