:: deftheorem Def23 defines final LATTICES:def 23 :
for L being non empty LattStr
for S being Subset of L holds
( S is final iff for p, q being Element of L st p [= q & p in S holds
q in S );