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 ROBBINS1:17;
hence (a + b) ` = (a `) *' (b `) by ROBBINS1:3; :: thesis: verum