theorem :: RMOD_3:27
for R being Ring
for V being RightMod of R
for W1, W2, W3 being Submodule of V holds (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3) by Lm10, RMOD_2:27;