theorem Th20: :: NORMSP_2:20

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