:: deftheorem Def18 defines complete LATTICE3:def 18 :
for IT being non empty LattStr holds
( IT is complete iff for X being set ex p being Element of IT st
( X is_less_than p & ( for r being Element of IT st X is_less_than r holds
p [= r ) ) );