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