let X be RealBanachSpace; :: thesis: for Y being Subset of X holds ClNLin Y is RealBanachSpace
let Y be Subset of X; :: thesis: ClNLin Y is RealBanachSpace
ex Z being Subset of X st
( Z = the carrier of (Lin Y) & ClNLin Y = NLin (Cl Z) & Cl Z is linearly-closed & Cl Z <> {} ) by Th35;
hence ClNLin Y is RealBanachSpace by NORMSP_3:49; :: thesis: verum