for V being RealLinearSpace
for W1, W2 being Subspace of V holds W1 /\ W2 is Subspace of W1 + W2 by Lm5, RLSUB_1:28;