theorem Th35: :: NORMSP_4:27

for X being RealBanachSpace
for Y being Subset of X 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 <> {} )