for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) by Lm4;