let G be addGroup; :: thesis: for g, h being Element of G holds
( g + h = h + g iff - (g + h) = (- g) + (- h) )
let g, h be Element of G; :: thesis: ( g + h = h + g iff - (g + h) = (- g) + (- h) )
thus ( g + h = h + g implies - (g + h) = (- g) + (- h) ) by Th16; :: thesis: ( - (g + h) = (- g) + (- h) implies g + h = h + g )
assume - (g + h) = (- g) + (- h) ; :: thesis: g + h = h + g
then A1: (h + g) + (- (g + h)) = ((h + g) + (- g)) + (- h) by RLVECT_1:def 3
.= (h + (g + (- g))) + (- h) by RLVECT_1:def 3
.= (h + (0_ G)) + (- h) by Def5
.= h + (- h) by Def4
.= 0_ G by Def5 ;
(g + h) + (- (g + h)) = 0_ G by Def5;
hence g + h = h + g by A1, Th6; :: thesis: verum