:: deftheorem Def16 defines Bottom LATTICES:def 16 :
for L being non empty /\-SemiLattStr st L is lower-bounded holds
for b₂ being Element of L holds
( b₂ = Bottom L iff for a being Element of L holds
( b₂ "/\" a = b₂ & a "/\" b₂ = b₂ ) );