let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a, b, c being Element of L holds a *' (b *' c) = (a *' b) *' c
let a, b, c be Element of L; :: thesis: a *' (b *' c) = (a *' b) *' c
thus (a *' b) *' c = (((a ` ) + (b ` )) + (c ` )) ` by Th3
.= ((a ` ) + ((b ` ) + (c ` ))) ` by LATTICES:def 5
.= a *' (b *' c) by Th3 ; :: thesis: verum