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 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 inf_net N is_eventually_in V ; :: thesis: N is_eventually_in V
then consider i being Element of (inf_net N) such that
A4: for j being Element of (inf_net N) st i <= j holds
(inf_net N) . j in V ;
consider j0 being Element of (inf_net N) such that
A5: i <= j0 and
i <= j0 by YELLOW_6:def 3;
A6: (inf_net N) . j0 in V by A4, A5;
reconsider j9 = j0 as Element of N by A3;
take j9 ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not j9 <= b₁ or N . b₁ in V )
let j be Element of N; :: thesis: ( not j9 <= j or N . j in V )
assume A7: j9 <= j ; :: thesis: N . j in V
defpred S₁[ Element of N] means $1 >= j9;
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] } ;
{ 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 ;
the mapping of (inf_net N) = f by A1, Def3;
then A8: (inf_net N) . j0 = "/\" (E,R) by A2;
N . j in E by A7;
then "/\" (E,R) <= N . j by Th8;
hence N . j in V by A6, A8, WAYBEL_0:def 20; :: thesis: verum