let T be non empty RelStr ; :: thesis: for N being net of T
for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )
let N be net of T; :: thesis: for X being set st N is_eventually_in X holds
ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )
let X be set ; :: thesis: ( N is_eventually_in X implies ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X ) )
given i9 being Element of N such that A1: for j being Element of N st j >= i9 holds
N . j in X ; :: according to WAYBEL_0:def 11 :: thesis: ex i being Element of N st
( N . i in X & rng the mapping of (N | i) c= X )
[#] N is directed by WAYBEL_0:def 6;
then consider i being Element of N such that
i in [#] N and
A2: i9 <= i and
i9 <= i ;
take i ; :: thesis: ( N . i in X & rng the mapping of (N | i) c= X )
thus N . i in X by A1, A2; :: thesis: rng the mapping of (N | i) c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng the mapping of (N | i) or x in X )
assume x in rng the mapping of (N | i) ; :: thesis: x in X
then consider j being object such that
A3: j in dom the mapping of (N | i) and
A4: x = the mapping of (N | i) . j by FUNCT_1:def 3;
A5: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def 1;
reconsider j = j as Element of (N | i) by A3;
the carrier of (N | i) = { y where y is Element of N : i <= y } by WAYBEL_9:12;
then consider k being Element of N such that
A6: j = k and
A7: i <= k by A3, A5;
x = (N | i) . j by A4
.= N . k by A6, WAYBEL_9:16 ;
hence x in X by A1, A2, A7, ORDERS_2:3; :: thesis: verum