let N be prenet of L; :: thesis: ( N is monotone implies N is eventually-directed )
assume A1: for i, j being Element of N st i <= j holds
for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds
a <= b ; :: according to ORDERS_3:def 5,WAYBEL_0:def 9 :: thesis: N is eventually-directed

now :: thesis: 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

let i be Element of N; :: thesis: ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k
take j = i; :: thesis: for k being Element of N st j <= k holds
N . i <= N . k
let k be Element of N; :: thesis: ( j <= k implies N . i <= N . k )
assume j <= k ; :: thesis: N . i <= N . k
hence N . i <= N . k by A1; :: thesis: verum

end;

hence N is eventually-directed by Th11; :: thesis: verum