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