thus ( G is Huntington implies for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ) by Def6; :: thesis: ( ( for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ) implies G is Huntington )
assume A1: for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ; :: thesis: G is Huntington
let x, y be Element of G; :: according to ROBBINS1:def 6 :: thesis: (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x
(((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x by A1;
hence (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x ; :: thesis: verum