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