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