let T be non empty 1-sorted ; :: thesis: for A being set

for N being net of T st N is_eventually_in A holds

for S being subnet of N holds S is_eventually_in A

let A be set ; :: thesis: for N being net of T st N is_eventually_in A holds

for S being subnet of N holds S is_eventually_in A

let N be net of T; :: thesis: ( N is_eventually_in A implies for S being subnet of N holds S is_eventually_in A )

given i being Element of N such that A1: for j being Element of N st i <= j holds

N . j in A ; :: according to WAYBEL_0:def 11 :: thesis: for S being subnet of N holds S is_eventually_in A

let S be subnet of N; :: thesis: S is_eventually_in A

consider f being Function of S,N such that

A2: the mapping of S = the mapping of N * f and

A3: for m being Element of N ex n being Element of S st

for p being Element of S st n <= p holds

m <= f . p by YELLOW_6:def 9;

consider n being Element of S such that

A4: for p being Element of S st n <= p holds

i <= f . p by A3;

take n ; :: according to WAYBEL_0:def 11 :: thesis: for b_{1} being Element of the carrier of S holds

( not n <= b_{1} or S . b_{1} in A )

let p be Element of S; :: thesis: ( not n <= p or S . p in A )

assume n <= p ; :: thesis: S . p in A

then N . (f . p) in A by A1, A4;

hence S . p in A by A2, FUNCT_2:15; :: thesis: verum

for N being net of T st N is_eventually_in A holds

for S being subnet of N holds S is_eventually_in A

let A be set ; :: thesis: for N being net of T st N is_eventually_in A holds

for S being subnet of N holds S is_eventually_in A

let N be net of T; :: thesis: ( N is_eventually_in A implies for S being subnet of N holds S is_eventually_in A )

given i being Element of N such that A1: for j being Element of N st i <= j holds

N . j in A ; :: according to WAYBEL_0:def 11 :: thesis: for S being subnet of N holds S is_eventually_in A

let S be subnet of N; :: thesis: S is_eventually_in A

consider f being Function of S,N such that

A2: the mapping of S = the mapping of N * f and

A3: for m being Element of N ex n being Element of S st

for p being Element of S st n <= p holds

m <= f . p by YELLOW_6:def 9;

consider n being Element of S such that

A4: for p being Element of S st n <= p holds

i <= f . p by A3;

take n ; :: according to WAYBEL_0:def 11 :: thesis: for b

( not n <= b

let p be Element of S; :: thesis: ( not n <= p or S . p in A )

assume n <= p ; :: thesis: S . p in A

then N . (f . p) in A by A1, A4;

hence S . p in A by A2, FUNCT_2:15; :: thesis: verum