let a, b be real number ; :: thesis:
set M = Closed-Interval-MSpace a,b;
assume A1: a <= b ; :: thesis:
reconsider a = a, b = b as Real by XREAL_0:def 1;
set r = b - a;

per cases by A1, XREAL_1:50;

suppose b - a = 0 ; :: thesis:

then ( [.a,b.] = {a} & the carrier of (Closed-Interval-TSpace a,b) = [.a,b.] ) by TOPMETR:25, XXREAL_1:17;
hence Closed-Interval-TSpace a,b is compact by COMPTS_1:27; :: thesis:

end;

suppose A2: b - a > 0 ; :: thesis:

A3: TopSpaceMetr (Closed-Interval-MSpace a,b) = Closed-Interval-TSpace a,b by TOPMETR:def 8;
assume not Closed-Interval-TSpace a,b is compact ; :: thesis:
then not Closed-Interval-MSpace a,b is compact by A3, TOPMETR:def 6;
then consider F being Subset-Family of (Closed-Interval-MSpace a,b) such that
A4: F is being_ball-family and
A5: F is Cover of (Closed-Interval-MSpace a,b) and
A6: for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not G is Cover of (Closed-Interval-MSpace a,b) or not G is finite ) by TOPMETR:23;
defpred S₁[ Element of NAT , Element of REAL , Element of REAL ] means ( ( ( for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G or not G is finite ) ) implies $3 = $2 - ((b - a) / (2 |^ ($1 + 2))) ) & ( ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G & G is finite ) implies $3 = $2 + ((b - a) / (2 |^ ($1 + 2))) ) );
A7: for n being Element of NAT
for p being Real ex w being Real st S₁[n,p,w]

proof

let n be Element of NAT ; :: thesis:
let p be Real; :: thesis:

now

per cases ;

suppose A8: for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G or not G is finite ) ; :: thesis:

take y = p - ((b - a) / (2 |^ (n + 2))); :: thesis:
thus S₁[n,p,y] by A8; :: thesis:

end;

suppose A9: ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G & G is finite ) ; :: thesis:

take y = p + ((b - a) / (2 |^ (n + 2))); :: thesis:
thus S₁[n,p,y] by A9; :: thesis:

end;

hence ex w being Real st S₁[n,p,w] ; :: thesis:

end;

consider f being Function of NAT ,REAL such that
A10: f . 0 = (a + b) / 2 and
A11: for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A7);
defpred S₂[ Element of NAT ] means for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.((f . $1) - ((b - a) / (2 |^ ($1 + 1)))),((f . $1) + ((b - a) / (2 |^ ($1 + 1)))).] c= union G or not G is finite );
A12: (f . 0 ) + ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) + ((b - a) / 2) by A10, NEWTON:10
.= b ;
defpred S₃[ Element of NAT ] means ( a <= (f . $1) - ((b - a) / (2 |^ ($1 + 1))) & (f . $1) + ((b - a) / (2 |^ ($1 + 1))) <= b );
A13: for n being Element of NAT holds
( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) )

proof

let n be Element of NAT ; :: thesis:
S₁[n,f . n,f . (n + 1)] by A11;
hence ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) ) ; :: thesis:

end;

A14: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of NAT ; :: thesis:
A15: ((b - a) / (2 * (2 |^ (k + 1)))) + ((b - a) / (2 * (2 |^ (k + 1)))) = (b - a) / (2 |^ (k + 1)) by XCMPLX_1:119;
A16: ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ (k + (1 + 1)))) = ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ ((k + 1) + 1)))
.= ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 * (2 |^ (k + 1)))) by NEWTON:11
.= (b - a) / (2 |^ ((k + 1) + 1)) by A15, NEWTON:11
.= (b - a) / (2 |^ (k + (1 + 1))) ;
assume A17: S₃[k] ; :: thesis:
then A18: b - (f . k) >= (b - a) / (2 |^ (k + 1)) by XREAL_1:21;
A19: (f . k) - a >= (b - a) / (2 |^ (k + 1)) by A17, XREAL_1:13;

now

per cases by A13;

suppose A20: f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) ; :: thesis:

( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then A21: (b - a) / (2 |^ (k + 1)) >= 0 ;
(f . (k + 1)) - a = ((f . k) - a) + ((b - a) / (2 |^ (k + 2))) by A20;
then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A19, A21, XREAL_1:33;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:13; :: thesis:
b - (f . (k + 1)) = (b - (f . k)) - ((b - a) / (2 |^ (k + 2))) by A20;
then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A18, A16, XREAL_1:11;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:21; :: thesis:

end;

suppose A22: f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ; :: thesis:

then (f . (k + 1)) - a = ((f . k) - a) - ((b - a) / (2 |^ (k + 2))) ;
then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A19, A16, XREAL_1:11;
hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:13; :: thesis:
( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then A23: (b - a) / (2 |^ (k + 1)) >= 0 ;
b - (f . (k + 1)) = (b - (f . k)) + ((b - a) / (2 |^ (k + 2))) by A22;
then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A18, A23, XREAL_1:33;
hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:21; :: thesis:

end;

hence S₃[k + 1] ; :: thesis:

end;

A24: (f . 0 ) - ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) - ((b - a) / 2) by A10, NEWTON:10
.= a ;
then A25: S₃[ 0 ] by A12;
A26: for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A25, A14);
A27: rng f c= [.a,b.]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f ; :: thesis:
then consider x being set such that
A28: x in dom f and
A29: y = f . x by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A28, FUNCT_2:def 1;
A30: ( 2 |^ (n + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
(f . n) + ((b - a) / (2 |^ (n + 1))) <= b by A26;
then A31: f . n <= b by A30, XREAL_1:42;
a <= (f . n) - ((b - a) / (2 |^ (n + 1))) by A26;
then a <= f . n by A30, XREAL_1:53;
then y in { y1 where y1 is Real : ( a <= y1 & y1 <= b ) } by A29, A31;
hence y in [.a,b.] by RCOMP_1:def 1; :: thesis:

end;

A32: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A33: S₂[k] ; :: thesis:
given G being Subset-Family of (Closed-Interval-MSpace a,b) such that A34: G c= F and
A35: [.((f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1)))),((f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1)))).] c= union G and
A36: G is finite ; :: thesis:
A37: (b - a) / (2 |^ (k + (1 + 1))) = (b - a) / (2 |^ ((k + 1) + 1))
.= (b - a) / ((2 |^ (k + 1)) * 2) by NEWTON:11
.= ((b - a) / (2 |^ (k + 1))) / 2 by XCMPLX_1:79 ;

now

per cases ;

suppose A38: ex G being Subset-Family of (Closed-Interval-MSpace a,b) st
( G c= F & [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G & G is finite ) ; :: thesis:

( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then ( (f . k) - ((b - a) / (2 |^ (k + 1))) <= f . k & f . k <= (f . k) + ((b - a) / (2 |^ (k + 1))) ) by XREAL_1:33, XREAL_1:45;
then A39: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] = [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] \/ [.(f . k),((f . k) + ((b - a) / (2 |^ (k + 1)))).] by XXREAL_1:165;
A40: (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38
.= f . k ;
consider G1 being Subset-Family of (Closed-Interval-MSpace a,b) such that
A41: G1 c= F and
A42: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G1 and
A43: G1 is finite by A38;
reconsider G3 = G1 \/ G as Subset-Family of (Closed-Interval-MSpace a,b) ;
(f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38
.= ((f . k) + (((b - a) / (2 |^ (k + 1))) / 2)) + (((b - a) / (2 |^ (k + 1))) / 2) by A37
.= (f . k) + ((b - a) / (2 |^ (k + 1))) ;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= (union G1) \/ (union G) by A35, A42, A40, A39, XBOOLE_1:13;
then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= union G3 by ZFMISC_1:96;
hence contradiction by A33, A34, A36, A41, A43, XBOOLE_1:8; :: thesis:

end;

suppose A44: for G being Subset-Family of (Closed-Interval-MSpace a,b) holds
( not G c= F or not [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G or not G is finite ) ; :: thesis:

then A45: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11
.= f . k ;
(f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A44
.= ((f . k) - (((b - a) / (2 |^ (k + 1))) / 2)) - (((b - a) / (2 |^ (k + 1))) / 2) by A37
.= (f . k) - ((b - a) / (2 |^ (k + 1))) ;
hence contradiction by A34, A35, A36, A44, A45; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A46: the carrier of (Closed-Interval-MSpace a,b) = [.a,b.] by A1, TOPMETR:14;
A47: S₂[ 0 ]

proof

given G being Subset-Family of (Closed-Interval-MSpace a,b) such that A48: G c= F and
A49: [.((f . 0 ) - ((b - a) / (2 |^ (0 + 1)))),((f . 0 ) + ((b - a) / (2 |^ (0 + 1)))).] c= union G and
A50: G is finite ; :: thesis:
the carrier of (Closed-Interval-MSpace a,b) c= union G by A1, A24, A12, A49, TOPMETR:14;
then G is Cover of (Closed-Interval-MSpace a,b) by SETFAM_1:def 12;
hence contradiction by A6, A48, A50; :: thesis:

end;

reconsider f = f as Real_Sequence ;
[.a,b.] is compact by RCOMP_1:24;
then consider s being Real_Sequence such that
A51: s is subsequence of f and
A52: s is convergent and
A53: lim s in [.a,b.] by A27, RCOMP_1:def 3;
reconsider ls = lim s as Point of (Closed-Interval-MSpace a,b) by A1, A53, TOPMETR:14;
consider Nseq being V36() sequence of NAT such that
A54: s = f * Nseq by A51, VALUED_0:def 17;
the carrier of (Closed-Interval-MSpace a,b) c= union F by A5, SETFAM_1:def 12;
then consider Z being set such that
A55: lim s in Z and
A56: Z in F by A53, A46, TARSKI:def 4;
consider p being Point of (Closed-Interval-MSpace a,b), r0 being Real such that
A57: Z = Ball p,r0 by A4, A56, TOPMETR:def 4;
set G = {(Ball p,r0)};
{(Ball p,r0)} c= bool the carrier of (Closed-Interval-MSpace a,b)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {(Ball p,r0)} ; :: thesis:
then a = Ball p,r0 by TARSKI:def 1;
hence a in bool the carrier of (Closed-Interval-MSpace a,b) ; :: thesis:

end;

then reconsider G = {(Ball p,r0)} as Subset-Family of (Closed-Interval-MSpace a,b) ;
A58: G c= F by A56, A57, ZFMISC_1:37;
reconsider Ns = Nseq as Real_Sequence by RELSET_1:17;
not Ns is bounded_above

proof

let r be real number ; :: according to SEQ_2:def 3 :: thesis:
consider n being Element of NAT such that
A59: n > r by SEQ_4:10;
rng Nseq c= NAT by VALUED_0:def 6;
then n <= Ns . n by Th6;
hence ex b₁ being Element of NAT st r <= Ns . b₁ by A59, XXREAL_0:2; :: thesis:

end;

then A60: 2 to_power Ns is divergent_to+infty by Th9, LIMFUNC1:58;
then A61: (2 to_power Ns) " is convergent by LIMFUNC1:61;
consider r1 being Real such that
A62: r1 > 0 and
A63: Ball ls,r1 c= Ball p,r0 by A55, A57, PCOMPS_1:30;
A64: r1 / 2 > 0 by A62, XREAL_1:141;
then consider n being Element of NAT such that
A65: for m being Element of NAT st m >= n holds
abs ((s . m) - (lim s)) < r1 / 2 by A52, SEQ_2:def 7;
A66: for m being Element of NAT
for q being Point of (Closed-Interval-MSpace a,b) st s . m = q & m >= n holds
dist ls,q < r1 / 2

proof

let m be Element of NAT ; :: thesis:
let q be Point of (Closed-Interval-MSpace a,b); :: thesis:
assume that
A67: s . m = q and
A68: m >= n ; :: thesis:
abs ((s . m) - (lim s)) < r1 / 2 by A65, A68;
then A69: abs (- ((s . m) - (lim s))) < r1 / 2 by COMPLEX1:138;
dist ls,q = the distance of (Closed-Interval-MSpace a,b) . (lim s),(s . m) by A67, METRIC_1:def 1
.= the distance of RealSpace . ls,q by A67, TOPMETR:def 1
.= abs ((lim s) - (s . m)) by A67, METRIC_1:def 13, METRIC_1:def 14 ;
hence dist ls,q < r1 / 2 by A69; :: thesis:

end;

A70: for m being Element of NAT st m >= n holds
(f * Nseq) . m in Ball ls,(r1 / 2)

proof

let m be Element of NAT ; :: thesis:
assume A71: m >= n ; :: thesis:
( dom f = NAT & s . m = f . (Nseq . m) ) by A54, FUNCT_2:21, FUNCT_2:def 1;
then s . m in rng f by FUNCT_1:def 5;
then reconsider q = s . m as Point of (Closed-Interval-MSpace a,b) by A1, A27, TOPMETR:14;
dist ls,q < r1 / 2 by A66, A71;
hence (f * Nseq) . m in Ball ls,(r1 / 2) by A54, METRIC_1:12; :: thesis:

end;

lim ((2 to_power Ns) " ) = 0 by A60, LIMFUNC1:61;
then A72: lim ((b - a) (#) ((2 to_power Ns) " )) = (b - a) * 0 by A61, SEQ_2:22
.= 0 ;
(b - a) (#) ((2 to_power Ns) " ) is convergent by A61, SEQ_2:21;
then consider i being Element of NAT such that
A73: for m being Element of NAT st i <= m holds
abs ((((b - a) (#) ((2 to_power Ns) " )) . m) - 0 ) < r1 / 2 by A64, A72, SEQ_2:def 7;
set l = (i + 1) + n;
A74: (i + 1) + n = (n + 1) + i ;
[.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] c= Ball ls,r1

proof

abs ((((b - a) (#) ((2 to_power Ns) " )) . ((i + 1) + n)) - 0 ) < r1 / 2 by A73, A74, NAT_1:11;
then abs ((b - a) * (((2 to_power Ns) " ) . ((i + 1) + n))) < r1 / 2 by SEQ_1:13;
then abs ((b - a) * (((2 to_power Ns) . ((i + 1) + n)) " )) < r1 / 2 by VALUED_1:10;
then abs ((b - a) * ((2 to_power (Ns . ((i + 1) + n))) " )) < r1 / 2 by Def1;
then A75: abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) " )) < r1 / 2 by POWER:46;
( 2 |^ ((Nseq . ((i + 1) + n)) + 1) = 2 * (2 |^ (Nseq . ((i + 1) + n))) & 2 |^ (Nseq . ((i + 1) + n)) > 0 ) by NEWTON:11, NEWTON:102;
then 1 / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) < (2 |^ (Nseq . ((i + 1) + n))) " by XREAL_1:90, XREAL_1:157;
then A76: (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) < (b - a) * ((2 |^ (Nseq . ((i + 1) + n))) " ) by A2, XREAL_1:70;
( 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) = (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) by ABSVALUE:def 1;
then abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) < abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) " )) by A76, ABSVALUE:12;
then A77: abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) < r1 / 2 by A75, XXREAL_0:2;
( 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:102, XREAL_1:50;
then A78: (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) < r1 / 2 by A77, ABSVALUE:def 1;
A79: s . ((i + 1) + n) in Ball ls,(r1 / 2) by A54, A70, NAT_1:11;
then reconsider sl = s . ((i + 1) + n) as Point of (Closed-Interval-MSpace a,b) ;
dist ls,sl < r1 / 2 by A79, METRIC_1:12;
then A80: abs ((lim s) - (s . ((i + 1) + n))) < r1 / 2 by Th1;
let z be set ; :: according to TARSKI:def 3 :: thesis:
A81: the carrier of (Closed-Interval-MSpace a,b) = [.a,b.] by A1, TOPMETR:14;
assume z in [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] ; :: thesis:
then z in { m where m is Real : ( (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) <= m & m <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) ) } by RCOMP_1:def 1;
then consider x being Real such that
A82: x = z and
A83: (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) <= x and
A84: x <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) ;
(f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) >= a by A26;
then (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) >= a by A54, FUNCT_2:21;
then A85: x >= a by A83, XXREAL_0:2;
(f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) <= b by A26;
then (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) <= b by A54, FUNCT_2:21;
then x <= b by A84, XXREAL_0:2;
then x in { m where m is Real : ( a <= m & m <= b ) } by A85;
then reconsider x9 = x as Point of (Closed-Interval-MSpace a,b) by A81, RCOMP_1:def 1;
abs ((lim s) - x) = abs (((lim s) - (s . ((i + 1) + n))) + ((s . ((i + 1) + n)) - x)) ;
then A86: abs ((lim s) - x) <= (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) by COMPLEX1:142;
x - (s . ((i + 1) + n)) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) by A84, XREAL_1:22;
then A87: - (x - (s . ((i + 1) + n))) >= - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) by XREAL_1:26;
s . ((i + 1) + n) <= ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " )) + x by A83, XREAL_1:22;
then (s . ((i + 1) + n)) - x <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) by XREAL_1:22;
then abs ((s . ((i + 1) + n)) - x) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ) by A87, ABSVALUE:12;
then abs ((s . ((i + 1) + n)) - x) < r1 / 2 by A78, XXREAL_0:2;
then (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) < (r1 / 2) + (r1 / 2) by A80, XREAL_1:10;
then abs ((lim s) - x) < (r1 / 2) + (r1 / 2) by A86, XXREAL_0:2;
then dist ls,x9 < r1 by Th1;
hence z in Ball ls,r1 by A82, METRIC_1:12; :: thesis:

end;

then [.((s . ((i + 1) + n)) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) " ))).] c= Ball p,r0 by A63, XBOOLE_1:1;
then [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball p,r0 by A54, FUNCT_2:21;
then [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball p,r0 by A54, FUNCT_2:21;
then A88: [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= union G by ZFMISC_1:31;
for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A47, A32);
hence contradiction by A58, A88; :: thesis:

end;

hence Closed-Interval-TSpace a,b is compact ; :: thesis: