theorem Th9: :: ROBBINS1:9

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds
( (Top L) ` = Bot L & Top L = (Bot L) ` )