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