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_{1} being Element of the carrier of N holds

( not i <= b_{1} or N . b_{1} 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

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

( not i <= b

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