theorem Th17: :: RMOD_3:17

for R being Ring
for V being RightMod of R
for W2 being Submodule of V holds
( ( for W1 being strict Submodule of V st W1 is Submodule of W2 holds
W1 /\ W2 = W1 ) & ( for W1 being Submodule of V st W1 /\ W2 = W1 holds
W1 is Submodule of W2 ) )