let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a being Element of L holds a + (Top L) = Top L
let a be Element of L; :: thesis: a + (Top L) = Top L
thus a + (Top L) = a + (a + (a `)) by Def8
.= (a + a) + (a `) by LATTICES:def 5
.= a + (a `) by Def7
.= Top L by Def8 ; :: thesis: verum