theorem :: ZMODUL01:48

for R being Ring
for V being strict LeftMod of R
for W being strict Submodule of V st ( for v being Vector of V holds
( v in W iff v in V ) ) holds
W = V