let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a being Element of L holds a + a = a
let a be Element of L; :: thesis: a + a = a
A1: (a + a) ` = ((((a ` ) ` ) + (a ` )) ` ) + ((a + a) ` ) by Th12
.= ((((a ` ) ` ) + (a ` )) ` ) + ((((a ` ) ` ) + a) ` ) by Th3
.= a ` by Def6 ;
thus a + a = ((a + a) ` ) ` by Th3
.= a by A1, Th3 ; :: thesis: verum