:: deftheorem Def12 defines complete LATTICE3:def 12 :
for IT being RelStr holds
( IT is complete iff for X being set ex a being Element of IT st
( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds
a <= b ) ) );