let S be non empty 1-sorted ; :: thesis: for N being net of S
for A being Subset of S,N holds N is_eventually_in A
let N be net of S; :: thesis: for A being Subset of S,N holds N is_eventually_in A
let A be Subset of S,N; :: thesis: N is_eventually_in A
consider i being Element of N such that
A1: A = rng the mapping of (N | i) by Def2;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not i <= b₁ or N . b₁ in A )
let j be Element of N; :: thesis: ( not i <= j or N . j in A )
assume i <= j ; :: thesis: N . j in A
then reconsider j9 = j as Element of (N | i) by WAYBEL_9:def 7;
N . j = (N | i) . j9 by WAYBEL_9:16
.= the mapping of (N | i) . j9 ;
hence N . j in A by A1, FUNCT_2:4; :: thesis: verum