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 Th8; :: thesis: verum