:: deftheorem Def9 defines Bot ROBBINS1:def 9 :
for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr
for b₂ being Element of L holds
( b₂ = Bot L iff for a being Element of L holds b₂ *' a = b₂ );