let L be complete Semilattice; :: thesis: ( ( for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) implies for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )

assume A1: for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; :: thesis: for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

let x be Element of L; :: thesis: for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

let N be prenet of L; :: thesis: ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )

assume A2: N is eventually-directed ; :: thesis: x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

reconsider R = rng (netmap (N,L)) as non empty directed Subset of L by A2, Th18;

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

set f = the mapping of N;

set h = the mapping of (FinSups the mapping of N);

A3: ex_sup_of xx "/\" R,L by WAYBEL_0:75;

A4: rng the mapping of (x "/\" (FinSups the mapping of N)) is_<=_than sup ({x} "/\" (rng (netmap (N,L))))

then rng (netmap ((x "/\" (FinSups the mapping of N)),L)) is directed by Th18;

then ex_sup_of rng the mapping of (x "/\" (FinSups the mapping of N)),L by WAYBEL_0:75;

then ( sup (x "/\" (FinSups the mapping of N)) = "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) & "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) <= sup ({x} "/\" (rng (netmap (N,L)))) ) by A4, YELLOW_0:def 9, YELLOW_2:def 5;

then A14: x "/\" (Sup ) <= sup ({x} "/\" (rng (netmap (N,L)))) by A1;

( ex_sup_of R,L & Sup = "\/" ((rng (netmap (N,L))),L) ) by WAYBEL_0:75, YELLOW_2:def 5;

then sup ({x} "/\" (rng (netmap (N,L)))) <= x "/\" (Sup ) by A3, YELLOW_4:53;

hence x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by A14, ORDERS_2:2; :: thesis: verum

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) implies for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )

assume A1: for x being Element of L

for J being set

for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ; :: thesis: for x being Element of L

for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

let x be Element of L; :: thesis: for N being prenet of L st N is eventually-directed holds

x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

let N be prenet of L; :: thesis: ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )

assume A2: N is eventually-directed ; :: thesis: x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))

reconsider R = rng (netmap (N,L)) as non empty directed Subset of L by A2, Th18;

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

set f = the mapping of N;

set h = the mapping of (FinSups the mapping of N);

A3: ex_sup_of xx "/\" R,L by WAYBEL_0:75;

A4: rng the mapping of (x "/\" (FinSups the mapping of N)) is_<=_than sup ({x} "/\" (rng (netmap (N,L))))

proof

x "/\" (FinSups the mapping of N) is eventually-directed
by Th27;
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in rng the mapping of (x "/\" (FinSups the mapping of N)) or a <= sup ({x} "/\" (rng (netmap (N,L)))) )

A5: {x} "/\" (rng the mapping of (FinSups the mapping of N)) = { (x "/\" y) where y is Element of L : y in rng the mapping of (FinSups the mapping of N) } by YELLOW_4:42;

assume a in rng the mapping of (x "/\" (FinSups the mapping of N)) ; :: thesis: a <= sup ({x} "/\" (rng (netmap (N,L))))

then a in {x} "/\" (rng the mapping of (FinSups the mapping of N)) by Th23;

then consider y being Element of L such that

A6: a = x "/\" y and

A7: y in rng the mapping of (FinSups the mapping of N) by A5;

for x being set holds ex_sup_of the mapping of N .: x,L by YELLOW_0:17;

then rng (netmap ((FinSups the mapping of N),L)) c= finsups (rng the mapping of N) by Th24;

then y in finsups (rng the mapping of N) by A7;

then consider Y being finite Subset of (rng the mapping of N) such that

A8: y = "\/" (Y,L) and

A9: ex_sup_of Y,L ;

rng (netmap (N,L)) is directed by A2, Th18;

then consider z being Element of L such that

A10: z in rng the mapping of N and

A11: z is_>=_than Y by WAYBEL_0:1;

A12: x <= x ;

"\/" (Y,L) <= z by A9, A11, YELLOW_0:30;

then A13: x "/\" y <= x "/\" z by A8, A12, YELLOW_3:2;

x in {x} by TARSKI:def 1;

then x "/\" z <= sup (xx "/\" (rng the mapping of N)) by A3, A10, YELLOW_4:1, YELLOW_4:37;

hence a <= sup ({x} "/\" (rng (netmap (N,L)))) by A6, A13, YELLOW_0:def 2; :: thesis: verum

end;A5: {x} "/\" (rng the mapping of (FinSups the mapping of N)) = { (x "/\" y) where y is Element of L : y in rng the mapping of (FinSups the mapping of N) } by YELLOW_4:42;

assume a in rng the mapping of (x "/\" (FinSups the mapping of N)) ; :: thesis: a <= sup ({x} "/\" (rng (netmap (N,L))))

then a in {x} "/\" (rng the mapping of (FinSups the mapping of N)) by Th23;

then consider y being Element of L such that

A6: a = x "/\" y and

A7: y in rng the mapping of (FinSups the mapping of N) by A5;

for x being set holds ex_sup_of the mapping of N .: x,L by YELLOW_0:17;

then rng (netmap ((FinSups the mapping of N),L)) c= finsups (rng the mapping of N) by Th24;

then y in finsups (rng the mapping of N) by A7;

then consider Y being finite Subset of (rng the mapping of N) such that

A8: y = "\/" (Y,L) and

A9: ex_sup_of Y,L ;

rng (netmap (N,L)) is directed by A2, Th18;

then consider z being Element of L such that

A10: z in rng the mapping of N and

A11: z is_>=_than Y by WAYBEL_0:1;

A12: x <= x ;

"\/" (Y,L) <= z by A9, A11, YELLOW_0:30;

then A13: x "/\" y <= x "/\" z by A8, A12, YELLOW_3:2;

x in {x} by TARSKI:def 1;

then x "/\" z <= sup (xx "/\" (rng the mapping of N)) by A3, A10, YELLOW_4:1, YELLOW_4:37;

hence a <= sup ({x} "/\" (rng (netmap (N,L)))) by A6, A13, YELLOW_0:def 2; :: thesis: verum

then rng (netmap ((x "/\" (FinSups the mapping of N)),L)) is directed by Th18;

then ex_sup_of rng the mapping of (x "/\" (FinSups the mapping of N)),L by WAYBEL_0:75;

then ( sup (x "/\" (FinSups the mapping of N)) = "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) & "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) <= sup ({x} "/\" (rng (netmap (N,L)))) ) by A4, YELLOW_0:def 9, YELLOW_2:def 5;

then A14: x "/\" (Sup ) <= sup ({x} "/\" (rng (netmap (N,L)))) by A1;

( ex_sup_of R,L & Sup = "\/" ((rng (netmap (N,L))),L) ) by WAYBEL_0:75, YELLOW_2:def 5;

then sup ({x} "/\" (rng (netmap (N,L)))) <= x "/\" (Sup ) by A3, YELLOW_4:53;

hence x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by A14, ORDERS_2:2; :: thesis: verum