theorem :: ZMODUL01:56

for R being Ring
for V being LeftMod of R holds V is Submodule of (Omega). V by VECTSP_4:41;