let M be non empty Abelian addMagma ; :: thesis: ( M is left_add-cancelable implies M is right_add-cancelable )
assume A2: M is left_add-cancelable ; :: thesis: M is right_add-cancelable
let x, y, z be Element of M; :: according to ALGSTR_0:def 4,ALGSTR_0:def 7 :: thesis: ( not y + x = z + x or y = z )
assume y + x = z + x ; :: thesis: y = z
hence y = z by A2, ALGSTR_0:def 3; :: thesis: verum