let S be non empty 1-sorted ; :: thesis: for N being net of S
for X being set
for M being subnet of N st M = N " X holds
M is_eventually_in X
let N be net of S; :: thesis: for X being set
for M being subnet of N st M = N " X holds
M is_eventually_in X
let X be set ; :: thesis: for M being subnet of N st M = N " X holds
M is_eventually_in X
let M be subnet of N; :: thesis: ( M = N " X implies M is_eventually_in X )
assume A1: M = N " X ; :: thesis: M is_eventually_in X
consider i being Element of M;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of M holds
( not i <= b₁ or M . b₁ in X )
let j be Element of M; :: thesis: ( not i <= j or M . j in X )
assume i <= j ; :: thesis: M . j in X
j in the carrier of M ;
then j in the mapping of N " X by A1, Def13;
then A2: the mapping of N . j in X by FUNCT_1:def 13;
the mapping of M = the mapping of N | the carrier of M by A1, Def8;
hence M . j in X by A2, FUNCT_1:72; :: thesis: verum