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)
hence (- g) + (- h) = - (g + h) by Th16
.= (- h) + (- g) by A1, Th17 ;
:: thesis: verum

end;

assume A2: (- g) + (- h) = (- h) + (- g) ; :: thesis: g + h = h + g
thus g + h = - (- (g + h))
.= - ((- h) + (- g)) by Th16
.= (- (- h)) + (- (- g)) by A2, Th16
.= h + g ; :: thesis: verum