theorem Tsym: :: LMOD_XX1:11
for R being Ring
for M, N being LeftMod of R st M ~= N holds
N ~= M