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