let G be non empty join-commutative join-associative Robbins ComplLLattStr ; :: thesis: ( ex c, d being Element of G st c + d = c implies G is Huntington )
A1: now :: thesis: for x, y, z being Element of G holds - ((- (((- ((- x) + y)) + x) + y)) + y) = - ((- x) + y)
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;
A2: now :: thesis: for x, y, z being Element of G holds z = - ((- (((- (((- ((- x) + y)) + x) + y)) + y) + z)) + (- ((- ((- x) + y)) + z)))
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 A1;
hence z = - ((- (((- (((- ((- x) + y)) + x) + y)) + y) + z)) + (- ((- ((- x) + y)) + z))) by Def5; :: thesis: verum
end;
given C, D being Element of G such that A3: C + D = C ; :: thesis: G is Huntington
A4: now :: thesis: for x, y, z being Element of G holds - ((- (((- ((- x) + y)) + (- (x + y))) + z)) + (- (y + z))) = z
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 :: thesis: for x being Element of G holds D = - ((- C) + (- ((D + (- (C + (- x)))) + (- (C + x)))))
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 A3, LATTICES:def 5 ; :: thesis: verum
end;
set e = - (C + (- C));
set K = - ((C + C) + (- (C + (- C))));
A6: - ((C + C) + (- (C + (- C)))) = - ((C + (- (C + (- C)))) + C) by LATTICES:def 5;
A7: now :: thesis: for x, y being Element of G holds - ((- ((D + (- (C + x))) + y)) + (- ((C + x) + y))) = D + y
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 A3, 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;
set L = - (D + (- C));
set E = D + (- C);
A8: - ((- C) + (- (D + (- C)))) = D by A3, Def5;
then A9: - (D + (- (C + (- (D + (- C)))))) = - (D + (- C)) by Def5;
- ((- (D + (- C))) + (- (C + (- (D + (- C)))))) = - ((- (D + (- (C + (- (D + (- C))))))) + (- ((D + C) + (- (D + (- C)))))) by A3, A8, Def5
.= - ((- (D + (- (C + (- (D + (- C))))))) + (- (D + (C + (- (D + (- C))))))) by LATTICES:def 5
.= D by Def5 ;
then - (D + (- ((D + (- C)) + (- (C + (- (D + (- C)))))))) = - (C + (- (D + (- C)))) by Def5;
then A10: - (C + (- (D + (- C)))) = - (D + (- ((D + (- (C + (- (D + (- C)))))) + (- C)))) by LATTICES:def 5
.= - C by A8, A9, Def5 ;
set L = C + (- (D + (- C)));
A11: C = - ((- ((D + (- (C + (- (D + (- C)))))) + C)) + (- ((- (D + (- C))) + C))) by A9, Def5
.= - ((- (C + (- (D + (- C))))) + (- (C + (- (C + (- (D + (- C)))))))) by A3, LATTICES:def 5 ;
then - (C + (- (C + (- (C + (- C)))))) = - (C + (- C)) by A10, Def5;
then C = - ((- (C + (- C))) + (- ((C + C) + (- (C + (- C)))))) by A6, 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 A11, A2, A10 ;
then D + (- (C + (- C))) = - ((- ((D + (- (C + C))) + (- (C + (- C))))) + (- C)) by A7
.= - ((- C) + (- ((D + (- (C + (- C)))) + (- (C + C))))) by LATTICES:def 5
.= D by A5 ;
then A12: C + (- (C + (- C))) = C by A3, LATTICES:def 5;
now :: thesis: for x being Element of G holds x = (- (C + (- C))) + x
let x be Element of G; :: thesis: x = (- (C + (- C))) + x
thus x = - ((- ((C + (- (C + (- C)))) + x)) + (- (((- C) + (- (C + (- C)))) + x))) by A11, A10, A12, 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;
then - (C + (- C)) = (- (C + (- C))) + (- (C + (- C))) ;
then G is with_idempotent_element ;
hence G is Huntington ; :: thesis: verum