:: deftheorem defines up-complete WAYBEL_0:def 39 :
for L being non empty reflexive RelStr holds
( L is up-complete iff for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) ) );