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)))
set f = the mapping of N;
reconsider R = rng (netmap N,L) as non empty directed Subset of L by A2, Th18;
A3: ex_sup_of R,L by WAYBEL_0:75;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
A4: ex_sup_of xx "/\" R,L by WAYBEL_0:75;
Sup = "\/" (rng (netmap N,L)),L by YELLOW_2:def 5;
then A5: sup ({x} "/\" (rng (netmap N,L))) <= x "/\" (Sup ) by A3, A4, YELLOW_4:53;
A6: sup (x "/\" (FinSups the mapping of N)) = "\/" (rng the mapping of (x "/\" (FinSups the mapping of N))),L by YELLOW_2:def 5;
set h = the mapping of (FinSups the mapping of N);
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 A7: ex_sup_of rng the mapping of (x "/\" (FinSups the mapping of N)),L by WAYBEL_0:75;
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))) )
assume a in rng the mapping of (x "/\" (FinSups the mapping of N)) ; :: thesis: a <= sup ({x} "/\" (rng (netmap N,L)))
then A8: a in {x} "/\" (rng the mapping of (FinSups the mapping of N)) by Th23;
{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;
then consider y being Element of L such that
A9: ( a = x "/\" y & y in rng the mapping of (FinSups the mapping of N) ) by A8;
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 A9;
then consider Y being finite Subset of (rng the mapping of N) such that
A10: ( y = "\/" Y,L & ex_sup_of Y,L ) ;
rng (netmap N,L) is directed by A2, Th18;
then consider z being Element of L such that
A11: ( z in rng the mapping of N & z is_>=_than Y ) by WAYBEL_0:1;
A12: "\/" Y,L <= z by A10, A11, YELLOW_0:30;
x in {x} by TARSKI:def 1;
then A13: x "/\" z <= sup (xx "/\" (rng the mapping of N)) by A4, A11, YELLOW_4:1, YELLOW_4:37;
x <= x ;
then x "/\" y <= x "/\" z by A10, A12, YELLOW_3:2;
hence a <= sup ({x} "/\" (rng (netmap N,L))) by A9, A13, YELLOW_0:def 2; :: thesis: verum

end;

then "\/" (rng the mapping of (x "/\" (FinSups the mapping of N))),L <= sup ({x} "/\" (rng (netmap N,L))) by A7, YELLOW_0:def 9;
then x "/\" (Sup ) <= sup ({x} "/\" (rng (netmap N,L))) by A1, A6;
hence x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L))) by A5, ORDERS_2:25; :: thesis: verum