for V being RealUnitarySpace
for W1 being Subspace of V
for W2 being strict Subspace of V holds W2 /\ (W2 + W1) = W2 by Lm7, RUSUB_1:24;