let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: 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:18;
hence (a + b) ` = (a ` ) *' (b ` ) by ROBBINS1:3; :: thesis: verum