theorem :: RLSUB_1:34

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