let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a, b being Element of L holds a + ((b + (b `)) `) = a
let a, b be Element of L; :: thesis: a + ((b + (b `)) `) = a
set O = b + (b `);
A1: ((b + (b `)) `) ` = b + (b `) by Th3;
A2: (b + (b `)) ` = (((((b + (b `)) `) `) + (((b + (b `)) `) `)) `) + (((((b + (b `)) `) `) + ((b + (b `)) `)) `) by Def6
.= (((b + (b `)) + (b + (b `))) `) + ((b + (b `)) `) by A1, Th4 ;
A3: b + (b `) = (a `) + a by Th4;
b + (b `) = (b + (b `)) + ((b + (b `)) `) by Th4
.= ((b + (b `)) + ((b + (b `)) `)) + (((b + (b `)) + (b + (b `))) `) by A2, LATTICES:def 5
.= (b + (b `)) + (((b + (b `)) + (b + (b `))) `) by Th4 ;
then A4: (b + (b `)) + (b + (b `)) = ((b + (b `)) + (b + (b `))) + (((b + (b `)) + (b + (b `))) `) by LATTICES:def 5
.= b + (b `) by Th4 ;
hence a + ((b + (b `)) `) = ((((a `) + (a `)) `) + (((a `) + a) `)) + ((((a `) + a) `) + (((a `) + a) `)) by A2, A3, Def6
.= (((a `) + (a `)) `) + ((((a `) + a) `) + (((a `) + a) `)) by A2, A4, A3, LATTICES:def 5
.= a by A2, A4, A3, Def6 ;
:: thesis: verum