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