theorem :: RLSUB_1:39

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