theorem :: RMOD_2:32
for R being Ring
for V being strict RightMod of R
for W being strict Submodule of V st ( for v being Vector of V holds v in W ) holds
W = V