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 (x "/\" ()) ) 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 (x "/\" ()) ; :: 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 ;
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
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 ;
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 ;
then A13: x "/\" y <= x "/\" z by ;
x in {x} by TARSKI:def 1;
then x "/\" z <= sup (xx "/\" (rng the mapping of N)) by ;
hence a <= sup ({x} "/\" (rng (netmap (N,L)))) by ; :: thesis: verum
end;
x "/\" (FinSups the mapping of N) is eventually-directed by Th27;
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 ;
then A14: x "/\" () <= sup ({x} "/\" (rng (netmap (N,L)))) by A1;
( ex_sup_of R,L & Sup = "\/" ((rng (netmap (N,L))),L) ) by ;
then sup ({x} "/\" (rng (netmap (N,L)))) <= x "/\" () by ;
hence x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) by ; :: thesis: verum