let X be RealNormSpace; :: thesis: for Y being Subset of X
for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds
( Y is dense iff Z is dense )
let Y be Subset of X; :: thesis: for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds
( Y is dense iff Z is dense )
let Z be Subset of (LinearTopSpaceNorm X); :: thesis: ( Y = Z implies ( Y is dense iff Z is dense ) )
assume A1: Y = Z ; :: thesis: ( Y is dense iff Z is dense )

hereby :: thesis: ( Z is dense implies Y is dense )

assume Y is dense ; :: thesis: Z is dense
then Cl Z = [#] X by A1, EQCL1
.= [#] (LinearTopSpaceNorm X) by NORMSP_2:def 4 ;
hence Z is dense ; :: thesis: verum

end;

assume Z is dense ; :: thesis: Y is dense
then Cl Y = [#] (LinearTopSpaceNorm X) by A1, EQCL1
.= [#] X by NORMSP_2:def 4 ;
hence Y is dense ; :: thesis: verum