let L be complete LATTICE; :: thesis: ( L is continuous implies for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup )
assume A1: L is continuous ; :: thesis: for J being non empty set
for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let J be non empty set ; :: thesis: for K being non-empty ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let K be non-empty ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
let F be DoubleIndexedSet of K,L; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )
assume A2: for j being Element of J holds rng (F . j) is directed ; :: thesis: Inf = Sup

now :: thesis: for c being Element of L st c << Inf holds
c <= Sup

let c be Element of L; :: thesis: ( c << Inf implies c <= Sup )
assume A3: c << Inf ; :: thesis: c <= Sup
A4: for j being Element of J holds c << Sup

proof

let j be Element of J; :: thesis: c << Sup
Sup in rng (Sups ) by Th14;
then inf (rng (Sups )) <= Sup by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def 6;
hence c << Sup by A3, WAYBEL_3:2; :: thesis: verum

end;

ex f being Function st
( f in dom (Frege F) & ( for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) )

proof

defpred S₁[ object , object ] means ( $1 in J & $2 in K . $1 & ex b being Element of L st
( b = (F . $1) . $2 & c <= b ) );
A5: for j being Element of J ex k being Element of K . j st c <= (F . j) . k

proof

let j be Element of J; :: thesis: ex k being Element of K . j st c <= (F . j) . k
A6: Sup <= sup (rng (F . j)) by YELLOW_2:def 5;
( rng (F . j) is non empty directed Subset of L & c << Sup ) by A2, A4;
then consider d being Element of L such that
A7: d in rng (F . j) and
A8: c <= d by A6, WAYBEL_3:def 1;
consider k being object such that
A9: k in dom (F . j) and
A10: d = (F . j) . k by A7, FUNCT_1:def 3;
reconsider k = k as Element of K . j by A9;
take k ; :: thesis: c <= (F . j) . k
thus c <= (F . j) . k by A8, A10; :: thesis: verum

end;

A11: for j being object st j in J holds
ex k being object st
( k in union (rng K) & S₁[j,k] )

proof

let j be object ; :: thesis: ( j in J implies ex k being object st
( k in union (rng K) & S₁[j,k] ) )
assume j in J ; :: thesis: ex k being object st
( k in union (rng K) & S₁[j,k] )
then reconsider j9 = j as Element of J ;
consider k being Element of K . j9 such that
A12: c <= (F . j9) . k by A5;
take k ; :: thesis: ( k in union (rng K) & S₁[j,k] )
j9 in J ;
then j9 in dom K by PARTFUN1:def 2;
then K . j9 in rng K by FUNCT_1:def 3;
hence k in union (rng K) by TARSKI:def 4; :: thesis: S₁[j,k]
thus S₁[j,k] by A12; :: thesis: verum

end;

consider f being Function such that
A13: dom f = J and
rng f c= union (rng K) and
A14: for j being object st j in J holds
S₁[j,f . j] from FUNCT_1:sch 6(A11);

A15: now :: thesis: for x being object st x in dom (doms F) holds
f . x in (doms F) . x

let x be object ; :: thesis: ( x in dom (doms F) implies f . x in (doms F) . x )
assume x in dom (doms F) ; :: thesis: f . x in (doms F) . x
then A16: x in dom F by FUNCT_6:59;
then reconsider j = x as Element of J ;
(doms F) . x = dom (F . j) by A16, FUNCT_6:22
.= K . j by FUNCT_2:def 1 ;
hence f . x in (doms F) . x by A14; :: thesis: verum

end;

dom f = dom F by A13, PARTFUN1:def 2
.= dom (doms F) by FUNCT_6:59 ;
then f in product (doms F) by A15, CARD_3:9;
then A17: f in dom (Frege F) by PARTFUN1:def 2;
for j being Element of J holds
( f . j in K . j & ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) by A14;
hence ex f being Function st
( f in dom (Frege F) & ( for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ) ) by A17; :: thesis: verum

end;

then consider f being Function such that
A18: f in dom (Frege F) and
A19: for j being Element of J ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) ;
reconsider f = f as Element of product (doms F) by A18;
reconsider G = (Frege F) . f as Function of J, the carrier of L ;

now :: thesis: for j being Element of J holds c <= G . j

let j be Element of J; :: thesis: c <= G . j
j in J ;
then A20: j in dom F by PARTFUN1:def 2;
ex b being Element of L st
( b = (F . j) . (f . j) & c <= b ) by A19;
hence c <= G . j by A18, A20, Th9; :: thesis: verum

end;

then A21: c <= Inf by YELLOW_2:55;
set a = Inf ;
Inf in rng (Infs ) by Th14;
then Inf <= sup (rng (Infs )) by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def 5;
hence c <= Sup by A21, YELLOW_0:def 2; :: thesis: verum

end;

then A22: Inf <= Sup by A1, Th17;
Inf >= Sup by Th16;
hence Inf = Sup by A22, YELLOW_0:def 3; :: thesis: verum