theorem Th8: :: ROBBINS1:8

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr
for a being Element of L holds Bot L = (a + (a `)) `