thus ( G is Huntington implies for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ) ; :: 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