let G be non empty left_add-cancelable add-right-invertible Abelian addLoopStr ; :: thesis: for a being Element of G holds - (- a) = a

let a be Element of G; :: thesis: - (- a) = a

(- a) + a = 0. G by Def1;

hence - (- a) = a by Def1; :: thesis: verum

let a be Element of G; :: thesis: - (- a) = a

(- a) + a = 0. G by Def1;

hence - (- a) = a by Def1; :: thesis: verum