let G be addGroup; :: thesis: for g, h being Element of G holds
( g + h = h + g iff g + (- h) = (- h) + g )
let g, h be Element of G; :: thesis: ( g + h = h + g iff g + (- h) = (- h) + g )
thus ( g + h = h + g implies g + (- h) = (- h) + g ) :: thesis: ( g + (- h) = (- h) + g implies g + h = h + g )

proof

assume A1: g + h = h + g ; :: thesis: g + (- h) = (- h) + g
(g + (- h)) + ((- g) + h) = ((g + (- h)) + (- g)) + h by RLVECT_1:def 3
.= (g + ((- h) + (- g))) + h by RLVECT_1:def 3
.= (g + ((- g) + (- h))) + h by A1, Th18
.= ((g + (- g)) + (- h)) + h by RLVECT_1:def 3
.= ((0_ G) + (- h)) + h by Def5
.= (- h) + h by Def4
.= 0_ G by Def5 ;
then g + (- h) = - ((- g) + h) by Th11
.= (- h) + (- (- g)) by Th16 ;
hence g + (- h) = (- h) + g ; :: thesis: verum

end;

assume g + (- h) = (- h) + g ; :: thesis: g + h = h + g
then g + ((- h) + h) = ((- h) + g) + h by RLVECT_1:def 3;
then g + (0_ G) = ((- h) + g) + h by Def5;
then g = ((- h) + g) + h by Def4;
then g = (- h) + (g + h) by RLVECT_1:def 3;
then h + g = (h + (- h)) + (g + h) by RLVECT_1:def 3;
then h + g = (0_ G) + (g + h) by Def5;
hence g + h = h + g by Def4; :: thesis: verum