theorem LM76A: :: NORMSP_3:47

for V being RealBanachSpace
for V1 being SubRealNormSpace of V st ex CV1 being Subset of V st
( CV1 = the carrier of V1 & CV1 is closed ) holds
V1 is RealBanachSpace