let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: ( ( for z being Element of G holds - (- z) = z ) implies G is Huntington )
assume A1: for z being Element of G holds - (- z) = z ; :: thesis: G is Huntington
let x be Element of G; :: according to ROBBINS1:def 12 :: thesis: for y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y
let y be Element of G; :: thesis: (- ((- x) + (- y))) + (- (x + (- y))) = y
A2: - (- ((- ((- x) + (- y))) + (- (x + (- y))))) = - (- y) by Def5;
(- ((- x) + (- y))) + (- (x + (- y))) = - (- ((- ((- x) + (- y))) + (- (x + (- y))))) by A1
.= y by A1, A2 ;
hence (- ((- x) + (- y))) + (- (x + (- y))) = y ; :: thesis: verum