theorem Th58: :: ROBBINS2:58

for L being non empty ComplLLattStr
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