let R be /\-complete Semilattice; :: thesis: for N being net of R
for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
let N be net of R; :: thesis: for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
let V be lower Subset of R; :: thesis: ( N is_eventually_in V implies inf_net 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 N is_eventually_in V ; :: thesis: inf_net N is_eventually_in V
then consider i being Element of N such that
A3: for j being Element of N st i <= j holds
N . j in V by WAYBEL_0:def 11;
reconsider i' = i as Element of (inf_net N) by A2;
take i' ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (inf_net N) holds
( not i' <= b₁ or (inf_net N) . b₁ in V )
let j be Element of (inf_net N); :: thesis: ( not i' <= j or (inf_net N) . j in V )
assume A4: i' <= j ; :: thesis: (inf_net N) . j in V
reconsider j0 = j as Element of N by A2;
defpred S₁[ Element of N] means $1 >= j0;
deffunc H₁( Element of N) -> Element of the carrier of R = N . $1;
set E = { H₁(k) where k is Element of N : S₁[k] } ;
consider j1 being Element of N such that
A5: ( j1 >= j0 & j1 >= j0 ) by YELLOW_6:def 5;
{ H₁(k) where k is Element of N : S₁[k] } is Subset of R from DOMAIN_1:sch 8();
then reconsider E = { H₁(k) where k is Element of N : S₁[k] } as Subset of R ;
( i <= j0 & j0 <= j1 ) by A2, A4, A5, YELLOW_0:1;
then i <= j1 by YELLOW_0:def 2;
then A6: N . j1 in V by A3;
N . j1 in E by A5;
then A7: "/\" E,R <= N . j1 by Th12;
the mapping of (inf_net N) = f by A1, Def3;
then (inf_net N) . j = "/\" E,R by A1;
hence (inf_net N) . j in V by A6, A7, WAYBEL_0:def 19; :: thesis: verum