let L be non empty ComplLLattStr ; :: thesis: for x, z being Element of L st L is join-commutative & L is join-associative & L is Huntington holds

(z + x) *' (z + (x `)) = z

let x, z be Element of L; :: thesis: ( L is join-commutative & L is join-associative & L is Huntington implies (z + x) *' (z + (x `)) = z )

assume ( L is join-commutative & L is join-associative & L is Huntington ) ; :: thesis: (z + x) *' (z + (x `)) = z

then reconsider L9 = L as non empty join-commutative join-associative Huntington ComplLLattStr ;

reconsider z9 = z, x9 = x as Element of L9 ;

(z9 + x9) *' (z9 + (x9 `)) = z9 + (x9 *' (x9 `)) by ROBBINS1:31

.= z9 + (Bot L9) by ROBBINS1:15

.= z9 by ROBBINS1:13 ;

hence (z + x) *' (z + (x `)) = z ; :: thesis: verum

(z + x) *' (z + (x `)) = z

let x, z be Element of L; :: thesis: ( L is join-commutative & L is join-associative & L is Huntington implies (z + x) *' (z + (x `)) = z )

assume ( L is join-commutative & L is join-associative & L is Huntington ) ; :: thesis: (z + x) *' (z + (x `)) = z

then reconsider L9 = L as non empty join-commutative join-associative Huntington ComplLLattStr ;

reconsider z9 = z, x9 = x as Element of L9 ;

(z9 + x9) *' (z9 + (x9 `)) = z9 + (x9 *' (x9 `)) by ROBBINS1:31

.= z9 + (Bot L9) by ROBBINS1:15

.= z9 by ROBBINS1:13 ;

hence (z + x) *' (z + (x `)) = z ; :: thesis: verum