theorem CLTh39: :: NORMSP_3:70

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