theorem Cl01: :: NORMSP_3:13

for X being RealNormSpace
for Y being Subspace of X
for CY being Subset of X st CY = the carrier of Y holds
Cl CY is linearly-closed