theorem :: NORMSP_3:27

for V being RealNormSpace
for W being SubRealNormSpace of V holds W is Subspace of V