let T be non empty 1-sorted ; :: thesis: for A being set
for N being net of 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 st N is_eventually_in A holds
for S being subnet of N holds S is_eventually_in A
let N be net of ; :: thesis: ( N is_eventually_in A implies for S being subnet of N holds S is_eventually_in A )
given i being Element of such that A1: for j being Element of 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 ex n being Element of st
for p being Element of st n <= p holds
m <= f . p by YELLOW_6:def 12;
consider n being Element of such that
A4: for p being Element of st n <= p holds
i <= f . p by A3;
take n ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of S holds
( not n <= b₁ or S . b₁ in A )
let p be Element of ; :: 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:21; :: thesis: verum