theorem :: RMOD_2:70
for R being Ring
for V being RightMod of R
for W being Submodule of V holds the carrier of W is Coset of W