theorem :: RMOD_3:26

for R being Ring
for V being RightMod of R
for W2 being Submodule of V
for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1 by Lm9, RMOD_2:29;