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 i' being Element of N such that A1: for j being Element of N st j >= i' 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 & [#] N = the carrier of N ) by WAYBEL_0:def 6;
then consider i being Element of N such that
A2: ( i in [#] N & i' <= i & i' <= i ) by WAYBEL_0:def 1;
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 set ; :: 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 set such that
A3: ( j in dom the mapping of (N | i) & x = the mapping of (N | i) . j ) by FUNCT_1:def 5;
A4: 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
A5: ( j = k & i <= k ) by A3, A4;
x = (N | i) . j by A3
.= N . k by A5, WAYBEL_9:16 ;
hence x in X by A1, A2, A5, ORDERS_2:26; :: thesis: verum