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

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