let X be RealNormSpace; :: thesis: for Y being Subset of X
for Z being Subset of (MetricSpaceNorm X) st Y = Z holds
Cl Y = Cl Z
let Y be Subset of X; :: thesis: for Z being Subset of (MetricSpaceNorm X) st Y = Z holds
Cl Y = Cl Z
let Z be Subset of (MetricSpaceNorm X); :: thesis: ( Y = Z implies Cl Y = Cl Z )
assume A1: Y = Z ; :: thesis: Cl Y = Cl Z
consider S being Subset of (LinearTopSpaceNorm X) such that
A2: ( Y = S & Cl Y = Cl S ) by NORMSP_3:def 1;
A3: the carrier of (TopSpaceNorm X) = the carrier of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
consider D being Subset of (TopSpaceMetr (MetricSpaceNorm X)) such that
A4: ( D = Z & Cl Z = Cl D ) by Def1;
for p being set st p in the carrier of (LinearTopSpaceNorm X) holds
( p in Cl D iff for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G )
proof
let p be set ; :: thesis: ( p in the carrier of (LinearTopSpaceNorm X) implies ( p in Cl D iff for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G ) )
assume A5: p in the carrier of (LinearTopSpaceNorm X) ; :: thesis: ( p in Cl D iff for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G )
( ( for G being Subset of (TopSpaceMetr (MetricSpaceNorm X)) st G is open & p in G holds
D meets G ) iff for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G )
proof
hereby :: thesis: ( ( for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G ) implies for G being Subset of (TopSpaceMetr (MetricSpaceNorm X)) st G is open & p in G holds
D meets G )
assume A6: for G being Subset of (TopSpaceMetr (MetricSpaceNorm X)) st G is open & p in G holds
D meets G ; :: thesis: for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G
let G be Subset of (LinearTopSpaceNorm X); :: thesis: ( G is open & p in G implies S meets G )
assume A7: ( G is open & p in G ) ; :: thesis: S meets G
reconsider G0 = G as Subset of (TopSpaceMetr (MetricSpaceNorm X)) by NORMSP_2:def 4;
( G0 is open & p in G0 ) by A7, A3, NORMSP_2:def 4;
hence S meets G by A6, A2, A4, A1; :: thesis: verum
end;
assume A9: for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G ; :: thesis: for G being Subset of (TopSpaceMetr (MetricSpaceNorm X)) st G is open & p in G holds
D meets G
let G be Subset of (TopSpaceMetr (MetricSpaceNorm X)); :: thesis: ( G is open & p in G implies D meets G )
assume A10: ( G is open & p in G ) ; :: thesis: D meets G
reconsider G0 = G as Subset of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
( G0 is open & p in G0 ) by A10, A3, NORMSP_2:def 4;
hence D meets G by A9, A2, A4, A1; :: thesis: verum
end;
hence ( p in Cl D iff for G being Subset of (LinearTopSpaceNorm X) st G is open & p in G holds
S meets G ) by A5, PRE_TOPC:def 7, A3; :: thesis: verum
end;
hence Cl Y = Cl Z by A2, A4, PRE_TOPC:def 7, A3; :: thesis: verum