theorem Th16: :: NORMSP_2:16

for X being RealNormSpace
for V being Subset of X
for Vt being Subset of (TopSpaceNorm X) st V = Vt holds
( V is open iff Vt is open )