let X be RealBanachSpace; :: thesis: for M being non empty Subset of X st M is linearly-closed & M is closed holds
NLin M is RealBanachSpace
let M be non empty Subset of X; :: thesis: ( M is linearly-closed & M is closed implies NLin M is RealBanachSpace )
assume A1: ( M is linearly-closed & M is closed ) ; :: thesis: NLin M is RealBanachSpace
then the carrier of (NLin M) = M by LCL1;
hence NLin M is RealBanachSpace by A1, LM76A; :: thesis: verum