theorem Th11: :: WAYBEL_0:11

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 ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k )