theorem :: NORMSP_4:28

for X being RealBanachSpace
for Y being Subset of X holds ClNLin Y is RealBanachSpace