theorem Th35: :: ROBBINS1:35

for L being non empty join-commutative join-associative Huntington ComplLLattStr holds Bot L = Bottom (CLatt L)