theorem :: LMOD_6:20

for K being Ring
for M, N being LeftMod of K st M c= N holds
(0). N c= M by VECTSP_4:39;