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