theorem :: ZMODUL01:41

for R being Ring
for V, X being strict LeftMod of R st V is Submodule of X & X is Submodule of V holds
V = X by VECTSP_4:25;