theorem :: RLSUB_1:38

for V being RealLinearSpace
for W being Subspace of V holds (0). W is Subspace of V by Th27;