let L be complete LATTICE; :: thesis: ( L is continuous implies for J being non empty set

for K being V9() 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 V9() 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 V9() 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 V9() 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

Inf >= Sup by Th16;

hence Inf = Sup by A22, YELLOW_0:def 3; :: thesis: verum

for K being V9() 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 V9() 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 V9() 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 V9() 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

then A22:
Inf <= Sup
by A1, Th17;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

( 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 ) ) )

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 ;

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;assume A3: c << Inf ; :: thesis: c <= Sup

A4: for j being Element of J holds c << Sup

proof

ex f being Function st
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;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

( 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

then consider f being Function such that
defpred S_{1}[ 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

ex k being object st

( k in union (rng K) & S_{1}[j,k] )

A13: dom f = J and

rng f c= union (rng K) and

A14: for j being object st j in J holds

S_{1}[j,f . j]
from FUNCT_1:sch 6(A11);

.= 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;( 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

A11:
for j being object st j in J holds
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;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

ex k being object st

( k in union (rng K) & S

proof

consider f being Function such that
let j be object ; :: thesis: ( j in J implies ex k being object st

( k in union (rng K) & S_{1}[j,k] ) )

assume j in J ; :: thesis: ex k being object st

( k in union (rng K) & S_{1}[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_{1}[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_{1}[j,k]

thus S_{1}[j,k]
by A12; :: thesis: verum

end;( k in union (rng K) & S

assume j in J ; :: thesis: ex k being object st

( k in union (rng K) & S

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

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

thus S

A13: dom f = J and

rng f c= union (rng K) and

A14: for j being object st j in J holds

S

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

f . x in (doms F) . x

dom f =
dom F
by A13, PARTFUN1:def 2
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;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

.= 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

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

then A21:
c <= Inf
by YELLOW_2:55;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;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

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

Inf >= Sup by Th16;

hence Inf = Sup by A22, YELLOW_0:def 3; :: thesis: verum