theorem Th13: :: ROBBINS1:13

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