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
set i = the Element of M;
take the Element of M ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of M holds
( not the Element of M <= b₁ or M . b₁ in X )
let j be Element of M; :: thesis: ( not the Element of M <= j or M . j in X )
assume the Element of M <= j ; :: thesis: M . j in X
j in the carrier of M ;
then j in the mapping of N " X by A1, Def10;
then A2: the mapping of N . j in X by FUNCT_1:def 7;
the mapping of M = the mapping of N | the carrier of M by A1, Def6;
hence M . j in X by A2, FUNCT_1:49; :: thesis: verum