theorem :: C0SP3:29

for X being NormedLinearTopSpace
for RNS being RealNormSpace
for V being Subset of X
for W being Subset of RNS st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) & V = W holds
( V is closed iff W is closed )