for R being Ring
for V being LeftMod of R
for W2 being Submodule of V
for W1 being strict Submodule of V holds
( W1 is Submodule of W2 iff W1 /\ W2 = W1 ) by VECTSP_5:16;