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

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

hence
N is eventually-directed
by Th11; :: thesis: verumfor 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;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