let L be complete LATTICE; :: thesis: ( ( for J being non empty set st J in the_universe_of the carrier of L holds

for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds

for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup ) implies L is continuous )

assume A1: for J being non empty set st J in the_universe_of the carrier of L holds

for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds

for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup ; :: thesis: L is continuous

hence L is continuous ; :: thesis: verum

for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds

for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup ) implies L is continuous )

assume A1: for J being non empty set st J in the_universe_of the carrier of L holds

for K being V9() ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds

for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup ; :: thesis: L is continuous

now :: thesis: for x being Element of L holds x = sup (waybelow x)

then
( L is up-complete & L is satisfying_axiom_of_approximation )
by WAYBEL_3:def 5;set UN = the_universe_of the carrier of L;

let x be Element of L; :: thesis: x = sup (waybelow x)

set J = { j where j is non empty directed Subset of L : x <= sup j } ;

A2: the_universe_of the carrier of L = Tarski-Class (the_transitive-closure_of the carrier of L) by YELLOW_6:def 1;

reconsider UN = the_universe_of the carrier of L as universal set ;

A3: { j where j is non empty directed Subset of L : x <= sup j } c= bool the carrier of L

then A4: the carrier of L in UN by CLASSES1:def 1;

then bool the carrier of L in UN by CLASSES2:59;

then A5: { j where j is non empty directed Subset of L : x <= sup j } in UN by A3, CLASSES1:def 1;

x is_>=_than waybelow x by WAYBEL_3:9;

then A6: x >= sup (waybelow x) by YELLOW_0:32;

( {x} is non empty directed Subset of L & x <= sup {x} ) by WAYBEL_0:5, YELLOW_0:39;

then A7: {x} in { j where j is non empty directed Subset of L : x <= sup j } ;

then reconsider J = { j where j is non empty directed Subset of L : x <= sup j } as non empty set ;

set K = id J;

reconsider K = id J as ManySortedSet of J ;

A8: for j being Element of J holds K . j in UN

A9: for j being Element of J holds j is non empty directed Subset of L

not K . i is empty

deffunc H_{1}( object ) -> Element of bool [:(K . $1),(K . $1):] = id (K . $1);

ex F being Function st

( dom F = J & ( for j being object st j in J holds

F . j = H_{1}(j) ) )
from FUNCT_1:sch 3();

then consider F being Function such that

A10: dom F = J and

A11: for j being object st j in J holds

F . j = id (K . j) ;

reconsider F = F as ManySortedSet of J by A10, PARTFUN1:def 2, RELAT_1:def 18;

for j being object st j in dom F holds

F . j is Function

for j being object st j in J holds

F . j is Function of (K . j),((J --> the carrier of L) . j)

A15: for j being Element of J

for k being Element of K . j holds (F . j) . k = k

//\ (((Frege F) . f),L) <= sup (waybelow x)

x is_<=_than rng (Sups )

then A36: x <= Inf by YELLOW_2:def 6;

Sup = sup (rng (F . j)) by YELLOW_2:def 5

.= sup {x} by A16

.= x by YELLOW_0:39 ;

then x in rng (Sups ) by Th14;

then inf (rng (Sups )) <= x by YELLOW_2:22;

then Inf <= x by YELLOW_2:def 6;

then x = Inf by A36, ORDERS_2:2

.= Sup by A1, A5, A8, A20 ;

hence x = sup (waybelow x) by A32, A6, ORDERS_2:2; :: thesis: verum

end;let x be Element of L; :: thesis: x = sup (waybelow x)

set J = { j where j is non empty directed Subset of L : x <= sup j } ;

A2: the_universe_of the carrier of L = Tarski-Class (the_transitive-closure_of the carrier of L) by YELLOW_6:def 1;

reconsider UN = the_universe_of the carrier of L as universal set ;

A3: { j where j is non empty directed Subset of L : x <= sup j } c= bool the carrier of L

proof

( the carrier of L c= the_transitive-closure_of the carrier of L & the_transitive-closure_of the carrier of L in UN )
by A2, CLASSES1:2, CLASSES1:52;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { j where j is non empty directed Subset of L : x <= sup j } or u in bool the carrier of L )

assume u in { j where j is non empty directed Subset of L : x <= sup j } ; :: thesis: u in bool the carrier of L

then ex j being non empty directed Subset of L st

( u = j & x <= sup j ) ;

hence u in bool the carrier of L ; :: thesis: verum

end;assume u in { j where j is non empty directed Subset of L : x <= sup j } ; :: thesis: u in bool the carrier of L

then ex j being non empty directed Subset of L st

( u = j & x <= sup j ) ;

hence u in bool the carrier of L ; :: thesis: verum

then A4: the carrier of L in UN by CLASSES1:def 1;

then bool the carrier of L in UN by CLASSES2:59;

then A5: { j where j is non empty directed Subset of L : x <= sup j } in UN by A3, CLASSES1:def 1;

x is_>=_than waybelow x by WAYBEL_3:9;

then A6: x >= sup (waybelow x) by YELLOW_0:32;

( {x} is non empty directed Subset of L & x <= sup {x} ) by WAYBEL_0:5, YELLOW_0:39;

then A7: {x} in { j where j is non empty directed Subset of L : x <= sup j } ;

then reconsider J = { j where j is non empty directed Subset of L : x <= sup j } as non empty set ;

set K = id J;

reconsider K = id J as ManySortedSet of J ;

A8: for j being Element of J holds K . j in UN

proof

reconsider j = {x} as Element of J by A7;
let j be Element of J; :: thesis: K . j in UN

K . j in J ;

hence K . j in UN by A4, A3, CLASSES1:def 1; :: thesis: verum

end;K . j in J ;

hence K . j in UN by A4, A3, CLASSES1:def 1; :: thesis: verum

A9: for j being Element of J holds j is non empty directed Subset of L

proof

for i being object st i in J holds
let j be Element of J; :: thesis: j is non empty directed Subset of L

j in J ;

then ex j9 being non empty directed Subset of L st

( j9 = j & x <= sup j9 ) ;

hence j is non empty directed Subset of L ; :: thesis: verum

end;j in J ;

then ex j9 being non empty directed Subset of L st

( j9 = j & x <= sup j9 ) ;

hence j is non empty directed Subset of L ; :: thesis: verum

not K . i is empty

proof

then reconsider K = K as V9() ManySortedSet of J by PBOOLE:def 13;
let i be object ; :: thesis: ( i in J implies not K . i is empty )

assume i in J ; :: thesis: not K . i is empty

then reconsider i9 = i as Element of J ;

K . i = i9 ;

hence not K . i is empty by A9; :: thesis: verum

end;assume i in J ; :: thesis: not K . i is empty

then reconsider i9 = i as Element of J ;

K . i = i9 ;

hence not K . i is empty by A9; :: thesis: verum

deffunc H

ex F being Function st

( dom F = J & ( for j being object st j in J holds

F . j = H

then consider F being Function such that

A10: dom F = J and

A11: for j being object st j in J holds

F . j = id (K . j) ;

reconsider F = F as ManySortedSet of J by A10, PARTFUN1:def 2, RELAT_1:def 18;

for j being object st j in dom F holds

F . j is Function

proof

then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def 6;
let j be object ; :: thesis: ( j in dom F implies F . j is Function )

assume j in dom F ; :: thesis: F . j is Function

then F . j = id (K . j) by A11;

hence F . j is Function ; :: thesis: verum

end;assume j in dom F ; :: thesis: F . j is Function

then F . j = id (K . j) by A11;

hence F . j is Function ; :: thesis: verum

for j being object st j in J holds

F . j is Function of (K . j),((J --> the carrier of L) . j)

proof

then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def 15;
let j be object ; :: thesis: ( j in J implies F . j is Function of (K . j),((J --> the carrier of L) . j) )

assume j in J ; :: thesis: F . j is Function of (K . j),((J --> the carrier of L) . j)

then reconsider j = j as Element of J ;

A12: K . j is Subset of L by A9;

A13: F . j = id (K . j) by A11;

then rng (F . j) c= K . j ;

then rng (F . j) c= the carrier of L by A12, XBOOLE_1:1;

then A14: rng (F . j) c= (J --> the carrier of L) . j ;

dom (F . j) = K . j by A13;

hence F . j is Function of (K . j),((J --> the carrier of L) . j) by A14, FUNCT_2:2; :: thesis: verum

end;assume j in J ; :: thesis: F . j is Function of (K . j),((J --> the carrier of L) . j)

then reconsider j = j as Element of J ;

A12: K . j is Subset of L by A9;

A13: F . j = id (K . j) by A11;

then rng (F . j) c= K . j ;

then rng (F . j) c= the carrier of L by A12, XBOOLE_1:1;

then A14: rng (F . j) c= (J --> the carrier of L) . j ;

dom (F . j) = K . j by A13;

hence F . j is Function of (K . j),((J --> the carrier of L) . j) by A14, FUNCT_2:2; :: thesis: verum

A15: for j being Element of J

for k being Element of K . j holds (F . j) . k = k

proof

A16:
for j being Element of J holds rng (F . j) = j
let j be Element of J; :: thesis: for k being Element of K . j holds (F . j) . k = k

let k be Element of K . j; :: thesis: (F . j) . k = k

F . j = id (K . j) by A11;

hence (F . j) . k = k ; :: thesis: verum

end;let k be Element of K . j; :: thesis: (F . j) . k = k

F . j = id (K . j) by A11;

hence (F . j) . k = k ; :: thesis: verum

proof

A20:
for j being Element of J holds rng (F . j) is directed
let j be Element of J; :: thesis: rng (F . j) = j

hence rng (F . j) = j by A19, XBOOLE_0:def 10; :: thesis: verum

end;now :: thesis: for y being object st y in rng (F . j) holds

y in j

then A19:
rng (F . j) c= j
;y in j

let y be object ; :: thesis: ( y in rng (F . j) implies y in j )

assume y in rng (F . j) ; :: thesis: y in j

then consider x being object such that

A17: x in dom (F . j) and

A18: y = (F . j) . x by FUNCT_1:def 3;

x in K . j by A17;

then x in j ;

hence y in j by A15, A18; :: thesis: verum

end;assume y in rng (F . j) ; :: thesis: y in j

then consider x being object such that

A17: x in dom (F . j) and

A18: y = (F . j) . x by FUNCT_1:def 3;

x in K . j by A17;

then x in j ;

hence y in j by A15, A18; :: thesis: verum

now :: thesis: for x being object st x in j holds

x in rng (F . j)

then
j c= rng (F . j)
;x in rng (F . j)

let x be object ; :: thesis: ( x in j implies x in rng (F . j) )

assume x in j ; :: thesis: x in rng (F . j)

then x in K . j ;

then ( (F . j) . x = x & x in dom (F . j) ) by A15, FUNCT_2:def 1;

hence x in rng (F . j) by FUNCT_1:def 3; :: thesis: verum

end;assume x in j ; :: thesis: x in rng (F . j)

then x in K . j ;

then ( (F . j) . x = x & x in dom (F . j) ) by A15, FUNCT_2:def 1;

hence x in rng (F . j) by FUNCT_1:def 3; :: thesis: verum

hence rng (F . j) = j by A19, XBOOLE_0:def 10; :: thesis: verum

proof

for f being Function st f in dom (Frege F) holds
let j be Element of J; :: thesis: rng (F . j) is directed

rng (F . j) = j by A16;

hence rng (F . j) is directed by A9; :: thesis: verum

end;rng (F . j) = j by A16;

hence rng (F . j) is directed by A9; :: thesis: verum

//\ (((Frege F) . f),L) <= sup (waybelow x)

proof

then A32:
Sup <= sup (waybelow x)
by Th15;
let f be Function; :: thesis: ( f in dom (Frege F) implies //\ (((Frege F) . f),L) <= sup (waybelow x) )

assume A21: f in dom (Frege F) ; :: thesis: //\ (((Frege F) . f),L) <= sup (waybelow x)

set a = //\ (((Frege F) . f),L);

for D being non empty directed Subset of L st x <= sup D holds

ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d )

then //\ (((Frege F) . f),L) in waybelow x by WAYBEL_3:7;

hence //\ (((Frege F) . f),L) <= sup (waybelow x) by YELLOW_2:22; :: thesis: verum

end;assume A21: f in dom (Frege F) ; :: thesis: //\ (((Frege F) . f),L) <= sup (waybelow x)

set a = //\ (((Frege F) . f),L);

for D being non empty directed Subset of L st x <= sup D holds

ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d )

proof

then
//\ (((Frege F) . f),L) << x
by WAYBEL_3:def 1;
A22:
for j being Element of J holds f . j in K . j

.= J by PARTFUN1:def 2 ;

then reconsider f = f as Function of J, the carrier of L by A23, FUNCT_2:2;

let D be non empty directed Subset of L; :: thesis: ( x <= sup D implies ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d ) )

assume x <= sup D ; :: thesis: ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d )

then D in J ;

then reconsider D9 = D as Element of J ;

A27: Inf <= f . D9 by YELLOW_2:53;

f . D9 in K . D9 by A22;

then A28: f . D9 in D9 ;

.= dom ((Frege F) . f) by A21, Th8 ;

then //\ (((Frege F) . f),L) <= f . D9 by A27, A29, FUNCT_1:2;

hence ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d ) by A28; :: thesis: verum

end;proof

A23: dom f =
dom F
by A21, Th8
let j be Element of J; :: thesis: f . j in K . j

j in J ;

then j in dom F by PARTFUN1:def 2;

then f . j in dom (F . j) by A21, Th9;

hence f . j in K . j ; :: thesis: verum

end;j in J ;

then j in dom F by PARTFUN1:def 2;

then f . j in dom (F . j) by A21, Th9;

hence f . j in K . j ; :: thesis: verum

.= J by PARTFUN1:def 2 ;

now :: thesis: for y being object st y in rng f holds

y in the carrier of L

then
rng f c= the carrier of L
;y in the carrier of L

let y be object ; :: thesis: ( y in rng f implies y in the carrier of L )

assume y in rng f ; :: thesis: y in the carrier of L

then consider j being object such that

A24: j in dom f and

A25: y = f . j by FUNCT_1:def 3;

reconsider j = j as Element of J by A23, A24;

y in K . j by A22, A25;

then A26: y in j ;

j is Subset of L by A9;

hence y in the carrier of L by A26; :: thesis: verum

end;assume y in rng f ; :: thesis: y in the carrier of L

then consider j being object such that

A24: j in dom f and

A25: y = f . j by FUNCT_1:def 3;

reconsider j = j as Element of J by A23, A24;

y in K . j by A22, A25;

then A26: y in j ;

j is Subset of L by A9;

hence y in the carrier of L by A26; :: thesis: verum

then reconsider f = f as Function of J, the carrier of L by A23, FUNCT_2:2;

let D be non empty directed Subset of L; :: thesis: ( x <= sup D implies ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d ) )

assume x <= sup D ; :: thesis: ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d )

then D in J ;

then reconsider D9 = D as Element of J ;

A27: Inf <= f . D9 by YELLOW_2:53;

f . D9 in K . D9 by A22;

then A28: f . D9 in D9 ;

A29: now :: thesis: for j being object st j in dom f holds

((Frege F) . f) . j = f . j

dom f =
dom F
by A21, Th8
((Frege F) . f) . j = f . j

let j be object ; :: thesis: ( j in dom f implies ((Frege F) . f) . j = f . j )

assume A30: j in dom f ; :: thesis: ((Frege F) . f) . j = f . j

then reconsider j9 = j as Element of J ;

A31: f . j9 is Element of K . j9 by A22;

j in dom F by A21, A30, Th8;

hence ((Frege F) . f) . j = (F . j9) . (f . j9) by A21, Th9

.= f . j by A15, A31 ;

:: thesis: verum

end;assume A30: j in dom f ; :: thesis: ((Frege F) . f) . j = f . j

then reconsider j9 = j as Element of J ;

A31: f . j9 is Element of K . j9 by A22;

j in dom F by A21, A30, Th8;

hence ((Frege F) . f) . j = (F . j9) . (f . j9) by A21, Th9

.= f . j by A15, A31 ;

:: thesis: verum

.= dom ((Frege F) . f) by A21, Th8 ;

then //\ (((Frege F) . f),L) <= f . D9 by A27, A29, FUNCT_1:2;

hence ex d being Element of L st

( d in D & //\ (((Frege F) . f),L) <= d ) by A28; :: thesis: verum

then //\ (((Frege F) . f),L) in waybelow x by WAYBEL_3:7;

hence //\ (((Frege F) . f),L) <= sup (waybelow x) by YELLOW_2:22; :: thesis: verum

x is_<=_than rng (Sups )

proof

then
x <= inf (rng (Sups ))
by YELLOW_0:33;
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in rng (Sups ) or x <= b )

assume b in rng (Sups ) ; :: thesis: x <= b

then consider j being Element of J such that

A33: b = Sup by Th14;

j in J ;

then consider j9 being non empty directed Subset of L such that

A34: j9 = j and

A35: x <= sup j9 ;

b = sup (rng (F . j)) by A33, YELLOW_2:def 5

.= sup j9 by A16, A34 ;

hence x <= b by A35; :: thesis: verum

end;assume b in rng (Sups ) ; :: thesis: x <= b

then consider j being Element of J such that

A33: b = Sup by Th14;

j in J ;

then consider j9 being non empty directed Subset of L such that

A34: j9 = j and

A35: x <= sup j9 ;

b = sup (rng (F . j)) by A33, YELLOW_2:def 5

.= sup j9 by A16, A34 ;

hence x <= b by A35; :: thesis: verum

then A36: x <= Inf by YELLOW_2:def 6;

Sup = sup (rng (F . j)) by YELLOW_2:def 5

.= sup {x} by A16

.= x by YELLOW_0:39 ;

then x in rng (Sups ) by Th14;

then inf (rng (Sups )) <= x by YELLOW_2:22;

then Inf <= x by YELLOW_2:def 6;

then x = Inf by A36, ORDERS_2:2

.= Sup by A1, A5, A8, A20 ;

hence x = sup (waybelow x) by A32, A6, ORDERS_2:2; :: thesis: verum

hence L is continuous ; :: thesis: verum