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