let T be non empty RelStr ; :: thesis: for N being net of
for X being set st N is_eventually_in X holds
ex i being Element of st
( N . i in X & rng the mapping of (N | i) c= X )
let N be net of ; :: thesis: for X being set st N is_eventually_in X holds
ex i being Element of 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 st
( N . i in X & rng the mapping of (N | i) c= X ) )
given i' being Element of such that A1: for j being Element of st j >= i' holds
N . j in X ; :: according to WAYBEL_0:def 11 :: thesis: ex i being Element of 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 such that
i in [#] N and
A2: i' <= i and
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) and
A4: x = the mapping of (N | i) . j by FUNCT_1:def 5;
A5: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def 1;
reconsider j = j as Element of by A3;
the carrier of (N | i) = { y where y is Element of : i <= y } by WAYBEL_9:12;
then consider k being Element of 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:26; :: thesis: verum