for R being Ring
for V being LeftMod of R
for W1, W2, W3 being Subspace of V st W1 /\ W2 <> (0). V holds
(W1 + W3) /\ W2 <> (0). V