let N be prenet of L; :: thesis: ( N is antitone implies N is eventually-filtered )
assume A2: 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 WAYBEL_0:def 5,WAYBEL_0:def 10 :: thesis: N is eventually-filtered
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 A2; :: thesis: verum
end;
hence N is eventually-filtered by Th12; :: thesis: verum