:: deftheorem Def5 defines max LATTICE7:def 5 :
for L being finite LATTICE
for A being non empty Chain of L
for b₃ being Element of L holds
( b₃ = max A iff ( ( for x being Element of L st x in A holds
x <= b₃ ) & b₃ in A ) );