:: deftheorem defines is_directed_wrt WAYBEL_4:def 22 :
for L being RelStr
for X being Subset of L
for R being Relation of the carrier of L holds
( X is_directed_wrt R 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] in R & [y,z] in R ) );