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 )

A1: now :: thesis: for i being Element of N holds
( N is_eventually_in { (N . j) where j is Element of N : S₁[N . j] } iff ex k being Element of N st
for l being Element of N st k <= l holds
S₁[N . l] )

let i be Element of N; :: thesis: ( N is_eventually_in { (N . j) where j is Element of N : S₁[N . j] } iff ex k being Element of N st
for l being Element of N st k <= l holds
S₁[N . l] )
defpred S₁[ Element of L] means N . i <= $1;
thus ( N is_eventually_in { (N . j) where j is Element of N : S₁[N . j] } iff ex k being Element of N st
for l being Element of N st k <= l holds
S₁[N . l] ) from WAYBEL_0:sch 1(); :: thesis: verum

end;

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

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