theorem Th18: :: NORMSP_4:14

for X being RealNormSpace
for Y being Subset of X holds
( the carrier of (NLin Y) c= the carrier of (ClNLin Y) & ex Z being Subset of X st
( Z = the carrier of (NLin Y) & Cl Z = the carrier of (ClNLin Y) ) )