theorem Th9: :: RMOD_2:9

for x being object
for R being Ring
for V being RightMod of R
for W being Submodule of V st x in W holds
x in V