theorem :: LMOD_6:17

for K being Ring
for V, M being strict LeftMod of K st V c= M & M c= V holds
V = M by VECTSP_4:25;