let L be non empty RelStr ; :: thesis: 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 )

let N be non empty NetStr over L; :: thesis: ( 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 )

for k being Element of N st j <= k holds

N . i <= N . k ; :: thesis: N is eventually-directed

let i be Element of N; :: according to WAYBEL_0:def 13 :: thesis: N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j }

ex j being Element of N st

for k being Element of N st j <= k holds

N . i <= N . k by A3;

hence N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A1; :: thesis: verum

( 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 )

let N be non empty NetStr over L; :: thesis: ( 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 )

A1: now :: thesis: for i being Element of N holds

( N is_eventually_in { (N . j) where j is Element of N : S_{1}[N . j] } iff ex k being Element of N st

for l being Element of N st k <= l holds

S_{1}[N . l] )

( N is_eventually_in { (N . j) where j is Element of N : S

for l being Element of N st k <= l holds

S

let i be Element of N; :: thesis: ( N is_eventually_in { (N . j) where j is Element of N : S_{1}[N . j] } iff ex k being Element of N st

for l being Element of N st k <= l holds

S_{1}[N . l] )

defpred S_{1}[ Element of L] means N . i <= $1;

thus ( N is_eventually_in { (N . j) where j is Element of N : S_{1}[N . j] } iff ex k being Element of N st

for l being Element of N st k <= l holds

S_{1}[N . l] )
from WAYBEL_0:sch 1(); :: thesis: verum

end;for l being Element of N st k <= l holds

S

defpred S

thus ( N is_eventually_in { (N . j) where j is Element of N : S

for l being Element of N st k <= l holds

S

hereby :: 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 ) implies N is eventually-directed )

assume A3:
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 ) implies N is eventually-directed )

assume A2:
N is eventually-directed
; :: 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

N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A2;

hence ex j being Element of N st

for k being Element of N st j <= k holds

N . i <= N . k by A1; :: thesis: verum

end;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

N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A2;

hence ex j being Element of N st

for k being Element of N st j <= k holds

N . i <= N . k by A1; :: thesis: verum

for k being Element of N st j <= k holds

N . i <= N . k ; :: thesis: N is eventually-directed

let i be Element of N; :: according to WAYBEL_0:def 13 :: thesis: N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j }

ex j being Element of N st

for k being Element of N st j <= k holds

N . i <= N . k by A3;

hence N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A1; :: thesis: verum