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₁ being Element of the carrier of S holds
( not n <= b₁ or S . b₁ 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