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