:: deftheorem Def4 defines Bot' SHEFFER1:def 4 :
for L being non empty LattStr st L is lower-bounded' holds
for b₂ being Element of L holds
( b₂ = Bot' L iff for a being Element of L holds
( b₂ "\/" a = a & a "\/" b₂ = a ) );