theorem Th1: :: DUALSP06:1

for V being RealNormSpace
for W being Subspace of V holds RSubNormSpace W is SubRealNormSpace of V