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

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