theorem Th1: :: NORMSP_4:1
for V being RealNormSpace
for V1 being SubRealNormSpace of V holds TopSpaceNorm V1 is SubSpace of TopSpaceNorm V