:: deftheorem defines complete LATTICE5:def 2 :
for L being non empty RelStr holds
( L is complete iff for X being Subset of L ex a being Element of L st
( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= a ) ) );