let G be non empty join-commutative join-associative Robbins ComplLattStr ; :: thesis: ( ex c, d being Element of G st c + d = c implies G is Huntington )
given C, D being Element of G such that A1: C + D = C ; :: thesis: G is Huntington
A2: - ((- C) + (- (D + (- C)))) = D by A1, Def5;

A3: now

let x, y be Element of G; :: thesis: - ((- ((D + (- (C + x))) + y)) + (- ((C + x) + y))) = D + y
thus - ((- ((D + (- (C + x))) + y)) + (- ((C + x) + y))) = - ((- ((- (C + x)) + (D + y))) + (- (((C + D) + x) + y))) by A1, LATTICES:def 5
.= - ((- ((- (C + x)) + (D + y))) + (- (((C + x) + D) + y))) by LATTICES:def 5
.= - ((- ((- (C + x)) + (D + y))) + (- ((C + x) + (D + y)))) by LATTICES:def 5
.= D + y by Def5 ; :: thesis: verum

end;

A4: now

let x, y, z be Element of G; :: thesis: - ((- (((- ((- x) + y)) + (- (x + y))) + z)) + (- (y + z))) = z
set k = (- ((- x) + y)) + (- (x + y));
thus - ((- (((- ((- x) + y)) + (- (x + y))) + z)) + (- (y + z))) = - ((- (((- ((- x) + y)) + (- (x + y))) + z)) + (- ((- ((- ((- x) + y)) + (- (x + y)))) + z))) by Def5
.= z by Def5 ; :: thesis: verum

end;

A5: now

let x, y, z be Element of G; :: thesis: - ((- (((- ((- x) + y)) + x) + y)) + y) = - ((- x) + y)
set k = - ((- x) + y);
thus - ((- (((- ((- x) + y)) + x) + y)) + y) = - ((- (((- ((- x) + y)) + x) + y)) + (- ((- ((- x) + y)) + (- (x + y))))) by Def5
.= - ((- ((- ((- x) + y)) + (x + y))) + (- ((- ((- x) + y)) + (- (x + y))))) by LATTICES:def 5
.= - ((- x) + y) by Def5 ; :: thesis: verum

end;

A6: now

let x be Element of G; :: thesis: D = - ((- C) + (- ((D + (- (C + (- x)))) + (- (C + x)))))
thus D = - ((- (((- ((- x) + C)) + (- (x + C))) + D)) + (- (C + D))) by A4
.= - ((- C) + (- ((D + (- (C + (- x)))) + (- (C + x))))) by A1, LATTICES:def 5 ; :: thesis: verum

end;

set E = D + (- C);
set L = - (D + (- C));
A7: - (D + (- (C + (- (D + (- C)))))) = - (D + (- C)) by A2, Def5;

now

thus - ((- (D + (- C))) + (- (C + (- (D + (- C)))))) = - ((- (D + (- (C + (- (D + (- C))))))) + (- ((D + C) + (- (D + (- C)))))) by A1, A2, Def5
.= - ((- (D + (- (C + (- (D + (- C))))))) + (- (D + (C + (- (D + (- C))))))) by LATTICES:def 5
.= D by Def5 ; :: thesis: verum

end;

then A8: - (D + (- ((D + (- C)) + (- (C + (- (D + (- C)))))))) = - (C + (- (D + (- C)))) by Def5;
set L = C + (- (D + (- C)));
A9: C = - ((- ((D + (- (C + (- (D + (- C)))))) + C)) + (- ((- (D + (- C))) + C))) by A7, Def5
.= - ((- (C + (- (D + (- C))))) + (- (C + (- (C + (- (D + (- C)))))))) by A1, LATTICES:def 5 ;

A10: now

let x, y, z be Element of G; :: thesis: z = - ((- (((- (((- ((- x) + y)) + x) + y)) + y) + z)) + (- ((- ((- x) + y)) + z)))
set k = - ((- x) + y);
- ((- (((- ((- x) + y)) + x) + y)) + y) = - ((- x) + y) by A5;
hence z = - ((- (((- (((- ((- x) + y)) + x) + y)) + y) + z)) + (- ((- ((- x) + y)) + z))) by Def5; :: thesis: verum

end;

A11: - (C + (- (D + (- C)))) = - (D + (- ((D + (- (C + (- (D + (- C)))))) + (- C)))) by A8, LATTICES:def 5
.= - C by A2, A7, Def5 ;
then A12: - (C + (- (C + (- (C + (- C)))))) = - (C + (- C)) by A9, Def5;
set K = - ((C + C) + (- (C + (- C))));
- ((C + C) + (- (C + (- C)))) = - ((C + (- (C + (- C)))) + C) by LATTICES:def 5;
then C = - ((- (C + (- C))) + (- ((C + C) + (- (C + (- C)))))) by A12, Def5;
then - (C + (- ((C + (- C)) + (- ((C + C) + (- (C + (- C)))))))) = - ((C + C) + (- (C + (- C)))) by Def5;
then - ((C + C) + (- (C + (- C)))) = - ((- (((- ((C + C) + (- (C + (- C))))) + C) + (- C))) + C) by LATTICES:def 5
.= - ((- (((- (((- (C + (- C))) + C) + C)) + C) + (- C))) + C) by LATTICES:def 5
.= - C by A9, A10, A11 ;
then D + (- (C + (- C))) = - ((- ((D + (- (C + C))) + (- (C + (- C))))) + (- C)) by A3
.= - ((- C) + (- ((D + (- (C + (- C)))) + (- (C + C))))) by LATTICES:def 5
.= D by A6 ;
then A13: C + (- (C + (- C))) = C by A1, LATTICES:def 5;

A14: now

let x be Element of G; :: thesis: x = (- (C + (- C))) + x
thus x = - ((- ((C + (- (C + (- C)))) + x)) + (- (((- C) + (- (C + (- C)))) + x))) by A9, A11, A13, Def5
.= - ((- (C + ((- (C + (- C))) + x))) + (- (((- C) + (- (C + (- C)))) + x))) by LATTICES:def 5
.= - ((- (C + ((- (C + (- C))) + x))) + (- ((- C) + ((- (C + (- C))) + x)))) by LATTICES:def 5
.= (- (C + (- C))) + x by Def5 ; :: thesis: verum

end;

set e = - (C + (- C));
- (C + (- C)) = (- (C + (- C))) + (- (C + (- C))) by A14;
then G is with_idempotent_element by Def13;
hence G is Huntington ; :: thesis: verum