theorem :: RUSUB_1:28

for V being RealUnitarySpace
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed by Lm1;