let L be complete LATTICE; :: thesis: ( ( for J, K being non empty set
for F being Function of [:J,K:], the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st
( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
holds
Inf = sup X ) implies L is continuous )

assume A1: for J, K being non empty set
for F being Function of [:J,K:], the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V9() ManySortedSet of J st
( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
holds
Inf = sup X ; :: thesis: L is continuous
for J, K being non empty set
for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng (() . j) is directed ) holds
Inf = Sup
proof
let J, K be non empty set ; :: thesis: for F being Function of [:J,K:], the carrier of L st ( for j being Element of J holds rng (() . j) is directed ) holds
Inf = Sup

let F be Function of [:J,K:], the carrier of L; :: thesis: ( ( for j being Element of J holds rng (() . j) is directed ) implies Inf = Sup )
assume A2: for j being Element of J holds rng (() . j) is directed ; :: thesis:
defpred S1[ Element of L] means ex f being V9() ManySortedSet of J st
( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being object st x in f . j holds
(G . j) . x = F . (j,x) ) & \$1 = Inf ) );
reconsider X = { a where a is Element of L : S1[a] } as Subset of L from X is_<=_than Sup
proof
let a9 be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a9 in X or a9 <= Sup )
assume a9 in X ; :: thesis: a9 <= Sup
then consider a being Element of L such that
A3: a9 = a and
A4: ex f being V9() ManySortedSet of J st
( f in Funcs (J,(Fin K)) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) ) ;
defpred S2[ object , object ] means ( \$1 in J & \$2 in K & ex b being Element of L st
( b = (() . \$1) . \$2 & a <= b ) );
consider f being V9() ManySortedSet of J such that
A5: f in Funcs (J,(Fin K)) and
A6: ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being object st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) by A4;
consider G being DoubleIndexedSet of f,L such that
A7: for j being Element of J
for x being object st x in f . j holds
(G . j) . x = F . (j,x) and
A8: a = Inf by A6;
A9: for x being object st x in J holds
ex y being object st
( y in K & S2[x,y] )
proof
let x be object ; :: thesis: ( x in J implies ex y being object st
( y in K & S2[x,y] ) )

assume x in J ; :: thesis: ex y being object st
( y in K & S2[x,y] )

then reconsider j = x as Element of J ;
Sup in rng () by Th14;
then inf (rng ()) <= Sup by YELLOW_2:22;
then A10: Inf <= Sup by YELLOW_2:def 6;
( not rng (() . j) is empty & rng (() . j) is directed & rng (G . j) is finite Subset of (rng (() . j)) ) by A2, A5, A7, Lm12;
then consider y being Element of L such that
A11: y in rng (() . j) and
A12: rng (G . j) is_<=_than y by WAYBEL_0:1;
consider k being object such that
A13: k in dom (() . j) and
A14: y = (() . j) . k by ;
reconsider k = k as Element of K by A13;
take k ; :: thesis: ( k in K & S2[x,k] )
sup (rng (G . j)) <= y by ;
then Sup <= y by YELLOW_2:def 5;
hence ( k in K & S2[x,k] ) by ; :: thesis: verum
end;
consider g being Function such that
A15: dom g = J and
rng g c= K and
A16: for x being object st x in J holds
S2[x,g . x] from A17: dom (doms ()) = dom () by FUNCT_6:59;
then A18: dom g = dom (doms ()) by ;
for x being object st x in dom (doms ()) holds
g . x in (doms ()) . x
proof
let x be object ; :: thesis: ( x in dom (doms ()) implies g . x in (doms ()) . x )
assume x in dom (doms ()) ; :: thesis: g . x in (doms ()) . x
then reconsider j = x as Element of J by A17;
dom () = J by Th20;
then (doms ()) . j = dom (() . j) by FUNCT_6:22
.= K by Th20 ;
hence g . x in (doms ()) . x by A16; :: thesis: verum
end;
then reconsider g = g as Element of product (doms ()) by ;
for j being Element of J holds a <= ((Frege ()) . g) . j
proof
let j be Element of J; :: thesis: a <= ((Frege ()) . g) . j
A19: ex b being Element of L st
( b = (() . j) . (g . j) & a <= b ) by A16;
( dom (Frege ()) = product (doms ()) & J = dom () ) by PARTFUN1:def 2;
hence a <= ((Frege ()) . g) . j by ; :: thesis: verum
end;
then A20: a <= Inf by YELLOW_2:55;
Inf in rng () by Th14;
then Inf <= sup (rng ()) by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def 5;
hence a9 <= Sup by ; :: thesis: verum
end;
then sup X <= Sup by YELLOW_0:32;
then A21: Inf <= Sup by A1;
Inf >= Sup by Th16;
hence Inf = Sup by ; :: thesis: verum
end;
hence L is continuous by Lm10; :: thesis: verum