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