let R be Ring; :: thesis: for M being LeftMod of R holds M ~= M
let M be LeftMod of R; :: thesis: M ~= M
A1: id M is Endomorphism of R,M by Def10;
id M is onto by RELAT_1:45;
hence M ~= M by A1; :: thesis: verum