let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: 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 ;
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 A3: (b + (b ` )) + (b + (b ` )) = ((b + (b ` )) + (b + (b ` ))) + (((b + (b ` )) + (b + (b ` ))) ` ) by LATTICES:def 5
.= b + (b ` ) by Th4 ;
A4: b + (b ` ) = (a ` ) + a 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, A3, A4, LATTICES:def 5
.= a by A2, A3, A4, Def6 ;
:: thesis: verum