theorem CLTh40: :: NORMSP_3:71

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