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