:: deftheorem Def1 defines directed WAYBEL_0:def 1 :
for L being RelStr
for X being Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) );