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 Th11
.= ((((a `) `) + (a `)) `) + ((((a `) `) + a) `) by Th3
.= a ` by Def6 ;
thus a + a = ((a + a) `) ` by Th3
.= a by A1, Th3 ; :: thesis: verum