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 and
A2: for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by Def4;
A3: 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
A4: for j being Element of N st i <= j holds
N . j in V ;
reconsider i9 = i as Element of (inf_net N) by A3;
take i9 ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (inf_net N) holds
( not i9 <= b₁ or (inf_net N) . b₁ in V )
let j be Element of (inf_net N); :: thesis: ( not i9 <= j or (inf_net N) . j in V )
assume A5: i9 <= j ; :: thesis: (inf_net N) . j in V
reconsider j0 = j as Element of N by A3;
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
A6: j1 >= j0 and
j1 >= j0 by YELLOW_6:def 3;
{ 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 by A3, A5, YELLOW_0:1;
then i <= j1 by A6, YELLOW_0:def 2;
then A7: N . j1 in V by A4;
N . j1 in E by A6;
then A8: "/\" (E,R) <= N . j1 by Th8;
the mapping of (inf_net N) = f by A1, Def3;
then (inf_net N) . j = "/\" (E,R) by A2;
hence (inf_net N) . j in V by A7, A8, WAYBEL_0:def 19; :: thesis: verum