:: deftheorem defines eventually-directed WAYBEL_0:def 13 :
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } );