let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a being Element of L holds a + (a `) = (a `) + ((a `) `)
let a be Element of L; :: thesis: a + (a `) = (a `) + ((a `) `)
set y = a ` ;
set z = ((a `) `) ` ;
( a = (((a `) + (((a `) `) `)) `) + (((a `) + ((a `) `)) `) & a ` = ((((a `) `) + (((a `) `) `)) `) + ((((a `) `) + ((a `) `)) `) ) by Def6;
then a + (a `) = (((((a `) + (((a `) `) `)) `) + (((a `) + ((a `) `)) `)) + ((((a `) `) + ((a `) `)) `)) + ((((a `) `) + (((a `) `) `)) `) by LATTICES:def 5
.= ((((((a `) `) + ((a `) `)) `) + (((a `) + ((a `) `)) `)) + (((a `) + (((a `) `) `)) `)) + ((((a `) `) + (((a `) `) `)) `) by LATTICES:def 5
.= (((((a `) `) + (a `)) `) + ((((a `) `) + ((a `) `)) `)) + ((((a `) + (((a `) `) `)) `) + ((((a `) `) + (((a `) `) `)) `)) by LATTICES:def 5
.= (a `) + ((((a `) + (((a `) `) `)) `) + ((((a `) `) + (((a `) `) `)) `)) by Def6
.= (a `) + ((a `) `) by Def6 ;
hence a + (a `) = (a `) + ((a `) `) ; :: thesis: verum