let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: thesis: ( ( for z being Element of holds - (- z) = z ) implies G is Huntington )
assume A1: for z being Element of holds - (- z) = z ; :: thesis: G is Huntington
let x be Element of ; :: according to ROBBINS1:def 12 :: thesis: for y being Element of holds (- ((- x) + (- y))) + (- (x + (- y))) = y
let y be Element of ; :: 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