let L be complete LATTICE; :: thesis:
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:

now :: thesis:

set UN = the_universe_of the carrier of L;
let x be Element of L; :: thesis:
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

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in { j where j is non empty directed Subset of L : x <= sup j } ; :: thesis:
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:

end;

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

let j be Element of J; :: thesis:
K . j in J ;
hence K . j in UN by A4, A3, CLASSES1:def 1; :: thesis:

end;

reconsider j = {x} as Element of J by A7;
A9: for j being Element of J holds j is non empty directed Subset of L

proof

let j be Element of J; :: thesis:
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:

end;

for i being object st i in J holds
not K . i is empty

proof

let i be object ; :: thesis:
assume i in J ; :: thesis:
then reconsider i9 = i as Element of J ;
K . i = i9 ;
hence not K . i is empty by A9; :: thesis:

end;

then reconsider K = K as V9() ManySortedSet of J by PBOOLE:def 13;
deffunc H₁( 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₁(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

proof

let j be object ; :: thesis:
assume j in dom F ; :: thesis:
then F . j = id (K . j) by A11;
hence F . j is Function ; :: thesis:

end;

then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def 6;
for j being object st j in J holds
F . j is Function of (K . j),((J --> the carrier of L) . j)

proof

let j be object ; :: thesis:
assume j in J ; :: thesis:
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:

end;

then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def 15;
A15: for j being Element of J
for k being Element of K . j holds (F . j) . k = k

proof

let j be Element of J; :: thesis:
let k be Element of K . j; :: thesis:
F . j = id (K . j) by A11;
hence (F . j) . k = k ; :: thesis:

end;

A16: for j being Element of J holds rng (F . j) = j

proof

let j be Element of J; :: thesis:

now :: thesis:

let y be object ; :: thesis:
assume y in rng (F . j) ; :: thesis:
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:

end;

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

now :: thesis:

let x be object ; :: thesis:
assume x in j ; :: thesis:
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:

end;

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

end;

A20: for j being Element of J holds rng (F . j) is directed

proof

let j be Element of J; :: thesis:
rng (F . j) = j by A16;
hence rng (F . j) is directed by A9; :: thesis:

end;

for f being Function st f in dom (Frege F) holds
//\ (((Frege F) . f),L) <= sup (waybelow x)

proof

let f be Function; :: thesis:
assume A21: f in dom (Frege F) ; :: thesis:
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

A22: for j being Element of J holds f . j in K . j

proof

let j be Element of J; :: thesis:
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:

end;

A23: dom f = dom F by A21, Th8
.= J by PARTFUN1:def 2 ;

now :: thesis:

let y be object ; :: thesis:
assume y in rng f ; :: thesis:
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:

end;

then rng f c= the carrier of L ;
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:
assume x <= sup D ; :: thesis:
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:

let j be object ; :: thesis:
assume A30: j in dom f ; :: thesis:
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:

end;

dom f = dom F by A21, Th8
.= 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:

end;

then //\ (((Frege F) . f),L) << x by WAYBEL_3:def 1;
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:

end;

then A32: Sup <= sup (waybelow x) by Th15;
x is_<=_than rng (Sups )

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis:
assume b in rng (Sups ) ; :: thesis:
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:

end;

then x <= inf (rng (Sups )) by YELLOW_0:33;
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:

end;

then ( L is up-complete & L is satisfying_axiom_of_approximation ) by WAYBEL_3:def 5;
hence L is continuous ; :: thesis: