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 )

then Cl Y = [#] (LinearTopSpaceNorm X) by A1, EQCL1

.= [#] X by NORMSP_2:def 4 ;

hence Y is dense ; :: thesis: verum

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
Z is dense
; :: thesis: 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;then Cl Z = [#] X by A1, EQCL1

.= [#] (LinearTopSpaceNorm X) by NORMSP_2:def 4 ;

hence Z is dense ; :: thesis: verum

then Cl Y = [#] (LinearTopSpaceNorm X) by A1, EQCL1

.= [#] X by NORMSP_2:def 4 ;

hence Y is dense ; :: thesis: verum