theorem :: RMOD_2:72

for R being Ring
for V being RightMod of R
for V1 being Subset of V st V1 is Coset of (Omega). V holds
V1 = the carrier of V