let R be /\-complete Semilattice; :: thesis: for N being net of R
for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
let N be net of R; :: thesis: for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
let V be upper Subset of R; :: thesis: ( inf_net N is_eventually_in V implies N is_eventually_in V )
consider f being Function of N,R such that
A1:
( inf_net N = N *' f & ( for i being Element of N holds f . i = "/\" { (N . k) where k is Element of N : k >= i } ,R ) )
by Def4;
A2:
RelStr(# the carrier of (inf_net N),the InternalRel of (inf_net N) #) = RelStr(# the carrier of N,the InternalRel of N #)
by A1, Def3;
assume
inf_net N is_eventually_in V
; :: thesis: N is_eventually_in V
then consider i being Element of (inf_net N) such that
A3:
for j being Element of (inf_net N) st i <= j holds
(inf_net N) . j in V
by WAYBEL_0:def 11;
consider j0 being Element of (inf_net N) such that
A4:
( i <= j0 & i <= j0 )
by YELLOW_6:def 5;
A5:
(inf_net N) . j0 in V
by A3, A4;
reconsider j' = j0 as Element of N by A2;
take
j'
; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not j' <= b1 or N . b1 in V )
let j be Element of N; :: thesis: ( not j' <= j or N . j in V )
assume A6:
j' <= j
; :: thesis: N . j in V
defpred S1[ Element of N] means $1 >= j';
deffunc H1( Element of N) -> Element of the carrier of R = N . $1;
set E = { H1(k) where k is Element of N : S1[k] } ;
{ H1(k) where k is Element of N : S1[k] } is Subset of R
from DOMAIN_1:sch 8();
then reconsider E = { H1(k) where k is Element of N : S1[k] } as Subset of R ;
the mapping of (inf_net N) = f
by A1, Def3;
then A7:
(inf_net N) . j0 = "/\" E,R
by A1;
N . j in E
by A6;
then
"/\" E,R <= N . j
by Th12;
hence
N . j in V
by A5, A7, WAYBEL_0:def 20; :: thesis: verum