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 set ; :: 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 by STRUCT_0:def 5;
then x in M2 by A1, Th16;
hence x in [#] M2 by STRUCT_0:def 5; :: thesis: verum