let K be Ring; :: thesis: for M1, M2 being LeftMod of K st M1 c= M2 holds
[#] M1 c= [#] M2
let M1, M2 be LeftMod of K; :: thesis: ( M1 c= M2 implies [#] M1 c= [#] M2 )
assume A1: M1 c= M2 ; :: thesis: [#] M1 c= [#] M2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] M1 or x in [#] M2 )
assume x in [#] M1 ; :: thesis: x in [#] M2
then x in M1 ;
then x in M2 by A1, Th14;
hence x in [#] M2 ; :: thesis: verum