let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a being Element of L holds a + (Bot L) = a
let a be Element of L; :: thesis: a + (Bot L) = a
a = (((a ` ) + (a ` )) ` ) + (((a ` ) + a) ` ) by Def6
.= ((a ` ) ` ) + (((a ` ) + a) ` ) by Def7
.= a + (((a ` ) + a) ` ) by Th3 ;
hence a + (Bot L) = a by Th9; :: thesis: verum