let L be non empty ComplLattStr ; :: 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 L' = L as non empty join-commutative join-associative Huntington ComplLattStr ;
reconsider z' = z, x' = x as Element of L' ;
(z' + x') *' (z' + (x' ` )) = z' + (x' *' (x' ` )) by ROBBINS1:32
.= z' + (Bot L') by ROBBINS1:16
.= z' by ROBBINS1:14 ;
hence (z + x) *' (z + (x ` )) = z ; :: thesis: verum