:: deftheorem defines complete VECTSP_8:def 6 :
for L being non empty LattStr holds
( L is complete iff for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) ) );