let a, b be Real_Sequence; :: thesis:
assume A1: for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ; :: thesis:
reconsider s = IntervalSequence (a,b) as SetSequence of (Euclid 1) by Th17;
A2: s is non-empty

proof

assume not s is non-empty ; :: thesis:
then consider i being object such that
A3: i in dom s and
A4: s . i = {} ;
product <*[.(a . i),(b . i).]*> = {} by A3, A4, Def1;
then {} in rng <*[.(a . i),(b . i).]*> by CARD_3:26;
then consider j being object such that
A5: j in dom <*[.(a . i),(b . i).]*> and
A6: <*[.(a . i),(b . i).]*> . j = {} by FUNCT_1:def 3;
j in {1} by FINSEQ_1:2, A5, FINSEQ_1:def 8;
then <*[.(a . i),(b . i).]*> . 1 = {} by A6, TARSKI:def 1;
then [.(a . i),(b . i).] is empty ;
hence contradiction by A1, A3, XXREAL_1:30; :: thesis:

end;

A7: s is pointwise_bounded

proof

now :: thesis:

let i be Nat; :: thesis:
A8: s . i = product <*[.(a . i),(b . i).]*> by Def1;
set si = product <*[.(a . i),(b . i).]*>;
reconsider si = product <*[.(a . i),(b . i).]*> as Subset of (Euclid 1) by A8;
ex r being Real st
( 0 < r & ( for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= r ) )

proof

set r = (b . i) - (a . i);

per cases ) - (a . i) = 0 or 0 < (b . i) - (a . i) ) by A1, XREAL_1:48;

suppose (b . i) - (a . i) = 0 ; :: thesis:

then A9: product <*[.(a . i),(b . i).]*> = product <*{(a . i)}*> by XXREAL_1:17
.= {<*(a . i)*>} by Th5 ;

now :: thesis:

take r = 1; :: thesis:
thus 0 < r ; :: thesis:

hereby :: thesis:

let x, y be Point of (Euclid 1); :: thesis:
assume ( x in si & y in si ) ; :: thesis:
then A10: ( x = <*(a . i)*> & y = <*(a . i)*> ) by A9, TARSKI:def 1;
Euclid 1 is Reflexive ;
hence dist (x,y) <= r by A10, METRIC_1:def 2; :: thesis:

end;

hence ex r being Real st
( 0 < r & ( for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= r ) ) ; :: thesis:

end;

suppose A11: 0 < (b . i) - (a . i) ; :: thesis:

take (b . i) - (a . i) ; :: thesis:
thus 0 < (b . i) - (a . i) by A11; :: thesis:

hereby :: thesis:

let x, y be Point of (Euclid 1); :: thesis:
assume that
A12: x in si and
A13: y in si ; :: thesis:
consider gx being Function such that
A14: x = gx and
dom gx = dom <*[.(a . i),(b . i).]*> and
A15: for j being object st j in dom <*[.(a . i),(b . i).]*> holds
gx . j in <*[.(a . i),(b . i).]*> . j by A12, CARD_3:def 5;
consider gy being Function such that
A16: y = gy and
dom gy = dom <*[.(a . i),(b . i).]*> and
A17: for j being object st j in dom <*[.(a . i),(b . i).]*> holds
gy . j in <*[.(a . i),(b . i).]*> . j by A13, CARD_3:def 5;
( x in Euclid 1 & y in Euclid 1 ) ;
then ( x in TOP-REAL 1 & y in TOP-REAL 1 ) by EUCLID:67;
then reconsider rx = x, ry = y as Element of REAL 1 by EUCLID:22;
Euclid 1 = MetrStruct(# (REAL 1),(Pitag_dist 1) #) by EUCLID:def 7;
then A18: dist (x,y) = |.(rx - ry).| by EUCLID:def 6;
consider ux being Real such that
A19: rx = <*ux*> by Th6;
consider uy being Real such that
A20: ry = <*uy*> by Th6;
( rx = 1 |-> ux & ry = 1 |-> uy ) by A19, A20, FINSEQ_2:59;
then A21: |.(rx - ry).| = (sqrt 1) * |.(ux - uy).| by TOPREALC:11
.= |.(ux - uy).| by SQUARE_1:18 ;
1 in Seg 1 by TARSKI:def 1, FINSEQ_1:2;
then 1 in dom <*[.(a . i),(b . i).]*> by FINSEQ_1:def 8;
then ( gx . 1 in <*[.(a . i),(b . i).]*> . 1 & gy . 1 in <*[.(a . i),(b . i).]*> . 1 ) by A15, A17;
then ( gx . 1 in [.(a . i),(b . i).] & gy . 1 in [.(a . i),(b . i).] ) ;
then ( ux in [.(a . i),(b . i).] & uy in [.(a . i),(b . i).] ) by A14, A16, A19, A20;
hence dist (x,y) <= (b . i) - (a . i) by A21, A18, UNIFORM1:12; :: thesis:

end;

then si is bounded ;
hence s . i is bounded by Def1; :: thesis:

end;

hence s is pointwise_bounded by COMPL_SP:def 1; :: thesis:

end;

s is closed

proof

for i being Nat holds s . i is closed

proof

let i be Nat; :: thesis:
A22: s . i = product <*[.(a . i),(b . i).]*> by Def1;
then reconsider si = product <*[.(a . i),(b . i).]*> as Subset of (Euclid 1) ;
A23: si ` = product <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>

proof

si ` = the carrier of (TOP-REAL 1) \ si by EUCLID:67
.= (REAL 1) \ (product <*[.(a . i),(b . i).]*>) by EUCLID:22
.= product <*(REAL \ [.(a . i),(b . i).])*> by Th18, SRINGS_4:27 ;
hence si ` = product <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> by XXREAL_1:385; :: thesis:

end;

si ` is open

proof

si ` in Family_open_set (Euclid 1)

proof

for x being Element of (Euclid 1) st x in si ` holds
ex r being Real st
( r > 0 & Ball (x,r) c= si ` )

proof

let x be Element of (Euclid 1); :: thesis:
assume A24: x in si ` ; :: thesis:
set A = ].-infty,(a . i).[;
set B = ].(b . i),+infty.[;
set f = <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>;
consider g being Function such that
A25: x = g and
dom g = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> and
A26: for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
g . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j by A24, A23, CARD_3:def 5;
1 in Seg 1 by TARSKI:def 1, FINSEQ_1:2;
then 1 in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> by FINSEQ_1:def 8;
then g . 1 in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . 1 by A26;
then g . 1 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[ ;

per cases by XBOOLE_0:def 3;

suppose A27: g . 1 in ].-infty,(a . i).[ ; :: thesis:

then reconsider g1 = g . 1 as ExtReal ;

now :: thesis:

x is Element of (TOP-REAL 1) by EUCLID:67;
then x is Element of REAL 1 by EUCLID:22;
then x in REAL 1 ;
then x in 1 -tuples_on REAL by EUCLID:def 1;
then g in Funcs ((Seg 1),REAL) by A25, FINSEQ_2:93;
then consider h being Function such that
A28: g = h and
A29: dom h = Seg 1 and
A30: rng h c= REAL by FUNCT_2:def 2;
1 in dom h by A29, TARSKI:def 1, FINSEQ_1:2;
then h . 1 in REAL by A30, FUNCT_1:3;
then reconsider g1 = g1 as Real by A28;
set r = |.(g1 - (a . i)).|;
take r = |.(g1 - (a . i)).|; :: thesis:
g1 - (a . i) <> 0 by A27, XXREAL_1:233;
hence r > 0 ; :: thesis:
thus Ball (x,r) c= si ` :: thesis:

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A31: t in Ball (x,r) ; :: thesis:
then reconsider t1 = t as Element of (Euclid 1) ;
( t1 in Euclid 1 & x in Euclid 1 ) ;
then ( t1 in TOP-REAL 1 & x in TOP-REAL 1 ) by EUCLID:67;
then reconsider rt1 = t1, rx = x as Element of REAL 1 by EUCLID:22;
Euclid 1 = MetrStruct(# (REAL 1),(Pitag_dist 1) #) by EUCLID:def 7;
then A32: dist (x,t1) = |.(rx - rt1).| by EUCLID:def 6;

now :: thesis:

take rt1 = rt1; :: thesis:
thus t = rt1 ; :: thesis:
rt1 in REAL 1 ;
then rt1 in 1 -tuples_on REAL by EUCLID:def 1;
then rt1 in Funcs ((Seg 1),REAL) by FINSEQ_2:93;
then consider h being Function such that
A33: rt1 = h and
A34: dom h = Seg 1 and
rng h c= REAL by FUNCT_2:def 2;
thus dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> by A33, A34, FINSEQ_1:def 8; :: thesis:

hereby :: thesis:

let j be object ; :: thesis:
assume j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> ; :: thesis:
then A35: j in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A36: j = 1 by TARSKI:def 1;
consider rt2 being Real such that
A37: rt1 = <*rt2*> by Th6;
A38: rt1 . j = rt1 . 1 by A35, TARSKI:def 1
.= rt2 by A37 ;
consider ux being Real such that
A39: rx = <*ux*> by Th6;
( rx = 1 |-> ux & rt1 = 1 |-> rt2 ) by A37, A39, FINSEQ_2:59;
then A40: |.(rx - rt1).| = (sqrt 1) * |.(ux - rt2).| by TOPREALC:11
.= |.(ux - rt2).| by SQUARE_1:18 ;
rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[

proof

A41: |.(ux - rt2).| < |.(g1 - (a . i)).| by A40, A32, A31, METRIC_1:11;
g1 - (a . i) < 0 by A27, XXREAL_1:233, XREAL_1:49;
then |.(g1 - (a . i)).| = - (g1 - (a . i)) by ABSVALUE:def 1;
then A42: |.(g1 - rt2).| < (a . i) - g1 by A25, A39, A41;

per cases ;

suppose 0 <= g1 - rt2 ; :: thesis:

then 0 + rt2 <= (g1 - rt2) + rt2 by XREAL_1:7;
then rt2 < a . i by A27, XXREAL_1:233, XXREAL_0:2;
then ( rt2 in ].-infty,(a . i).[ or rt2 in ].(b . i),+infty.[ ) by XXREAL_1:233;
hence rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[ by XBOOLE_0:def 3; :: thesis:

end;

suppose g1 - rt2 < 0 ; :: thesis:

then - (g1 - rt2) < (a . i) - g1 by A42, ABSVALUE:def 1;
then (rt2 - g1) + g1 < ((a . i) - g1) + g1 by XREAL_1:8;
then ( rt2 in ].-infty,(a . i).[ or rt2 in ].(b . i),+infty.[ ) by XXREAL_1:233;
hence rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[ by XBOOLE_0:def 3; :: thesis:

end;

hence rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j by A36, A38; :: thesis:

end;

hence t in si ` by A23, CARD_3:def 5; :: thesis:

end;

hence ex r being Real st
( r > 0 & Ball (x,r) c= si ` ) ; :: thesis:

end;

suppose A43: g . 1 in ].(b . i),+infty.[ ; :: thesis:

then reconsider g1 = g . 1 as ExtReal ;

now :: thesis:

x is Element of (TOP-REAL 1) by EUCLID:67;
then x is Element of REAL 1 by EUCLID:22;
then x in REAL 1 ;
then x in 1 -tuples_on REAL by EUCLID:def 1;
then g in Funcs ((Seg 1),REAL) by A25, FINSEQ_2:93;
then consider h being Function such that
A44: g = h and
A45: dom h = Seg 1 and
A46: rng h c= REAL by FUNCT_2:def 2;
1 in Seg 1 by TARSKI:def 1, FINSEQ_1:2;
then h . 1 in REAL by A45, A46, FUNCT_1:3;
then reconsider g1 = g1 as Real by A44;
set r = |.(g1 - (b . i)).|;
take r = |.(g1 - (b . i)).|; :: thesis:
g1 - (b . i) <> 0 by A43, XXREAL_1:235;
hence r > 0 ; :: thesis:
thus Ball (x,r) c= si ` :: thesis:

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A46bis: t in Ball (x,r) ; :: thesis:
then reconsider t1 = t as Element of (Euclid 1) ;
( t1 in Euclid 1 & x in Euclid 1 ) ;
then ( t1 in TOP-REAL 1 & x in TOP-REAL 1 ) by EUCLID:67;
then reconsider rt1 = t1, rx = x as Element of REAL 1 by EUCLID:22;
Euclid 1 = MetrStruct(# (REAL 1),(Pitag_dist 1) #) by EUCLID:def 7;
then A46ter: dist (x,t1) = |.(rx - rt1).| by EUCLID:def 6;

now :: thesis:

take rt1 = rt1; :: thesis:
thus t = rt1 ; :: thesis:
rt1 in REAL 1 ;
then rt1 in 1 -tuples_on REAL by EUCLID:def 1;
then rt1 in Funcs ((Seg 1),REAL) by FINSEQ_2:93;
then consider h being Function such that
A47: rt1 = h and
A48: dom h = Seg 1 and
rng h c= REAL by FUNCT_2:def 2;
thus dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> by A47, A48, FINSEQ_1:def 8; :: thesis:

hereby :: thesis:

let j be object ; :: thesis:
assume j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> ; :: thesis:
then A49: j in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A50: j = 1 by TARSKI:def 1;
consider rt2 being Real such that
A51: rt1 = <*rt2*> by Th6;
A52: rt1 . j = rt1 . 1 by A49, TARSKI:def 1
.= rt2 by A51 ;
consider ux being Real such that
A53: rx = <*ux*> by Th6;
( rx = 1 |-> ux & rt1 = 1 |-> rt2 ) by A51, A53, FINSEQ_2:59;
then A54: |.(rx - rt1).| = (sqrt 1) * |.(ux - rt2).| by TOPREALC:11
.= |.(ux - rt2).| by SQUARE_1:18 ;
rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[

proof

ux = g1 by A25, A53;
then A55: |.(g1 - rt2).| < |.(g1 - (b . i)).| by A54, A46bis, A46ter, METRIC_1:11;
0 < g1 - (b . i) by A43, XXREAL_1:235, XREAL_1:50;
then A56: |.(g1 - rt2).| < g1 - (b . i) by A55, ABSVALUE:def 1;
g1 - rt2 < g1 - (b . i) by A56, ABSVALUE:def 1;
then (g1 - rt2) - g1 < (g1 - (b . i)) - g1 by XREAL_1:14;
then - rt2 < - (b . i) ;
then ( rt2 in ].-infty,(a . i).[ or rt2 in ].(b . i),+infty.[ ) by XREAL_1:24, XXREAL_1:235;
hence rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[ by XBOOLE_0:def 3; :: thesis:

end;

hence rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j by A52, A50; :: thesis:

end;

hence t in si ` by A23, CARD_3:def 5; :: thesis:

end;

hence ex r being Real st
( r > 0 & Ball (x,r) c= si ` ) ; :: thesis:

end;

hence si ` in Family_open_set (Euclid 1) by PCOMPS_1:def 4; :: thesis:

end;

hence si ` is open by COMPL_SP:def 3; :: thesis:

end;

hence s . i is closed by A22, COMPL_SP:def 4; :: thesis:

end;

hence s is closed by COMPL_SP:def 8; :: thesis:

end;

hence IntervalSequence (a,b) is non-empty pointwise_bounded closed SetSequence of (Euclid 1) by A2, A7; :: thesis: