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