let M be non empty Abelian addLoopStr ; :: thesis: ( M is left_complementable implies M is right_complementable )
assume A3: M is left_complementable ; :: thesis: M is right_complementable
let x be Element of M; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
ex y being Element of M st y + x = 0. M by A3, ALGSTR_0:def 10;
hence x is right_complementable ; :: thesis: verum