theorem Th6: :: ROBBINS1:6

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds L is upper-bounded