for V being RealNormSpace
for V1 being SubRealNormSpace of V
for S being Subset of V st S = the carrier of V1 holds
S is linearly-closed