:: deftheorem Def8 defines Top ROBBINS1:def 8 :
for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr
for b₂ being M3( the carrier of b₁) holds
( b₂ = Top L iff ex a being Element of L st b₂ = a + (a `) );