:: deftheorem Def21 defines "\/" LATTICE3:def 21 :
for L being non empty LattStr st L is complete Lattice holds
for X being set
for b₃ being Element of L holds
( b₃ = "\/" (X,L) iff ( X is_less_than b₃ & ( for r being Element of L st X is_less_than r holds
b₃ [= r ) ) );