theorem Tref: :: LMOD_XX1:10

for R being Ring
for M being LeftMod of R holds M ~= M