theorem ThSubSpace: :: NORMSP_3:30

for V being RealNormSpace
for V1 being Subset of V holds NLin V1 is SubRealNormSpace of V