:: deftheorem Def2 defines Top' SHEFFER1:def 2 :
for L being non empty LattStr st L is upper-bounded' holds
for b₂ being Element of L holds
( b₂ = Top' L iff for a being Element of L holds
( b₂ "/\" a = a & a "/\" b₂ = a ) );