theorem :: NORMSP_3:49

for X being RealBanachSpace
for M being non empty Subset of X st M is linearly-closed & M is closed holds
NLin M is RealBanachSpace