let a, b be Real; :: thesis: for E being sequence of (bool REAL) st a < b & ( for n being Nat holds E . n = [.(a + ((b - a) / (n + 1))),b.] ) holds
( E is non-descending & E is convergent & Union E = ].a,b.] )
let E be sequence of (bool REAL); :: thesis: ( a < b & ( for n being Nat holds E . n = [.(a + ((b - a) / (n + 1))),b.] ) implies ( E is non-descending & E is convergent & Union E = ].a,b.] ) )
assume that
A1: a < b and
A2: for n being Nat holds E . n = [.(a + ((b - a) / (n + 1))),b.] ; :: thesis: ( E is non-descending & E is convergent & Union E = ].a,b.] )
A3: b - a > 0 by A1, XREAL_1:50;
for n, m being Nat st n <= m holds
E . n c= E . m

proof

let n, m be Nat; :: thesis: ( n <= m implies E . n c= E . m )
assume n <= m ; :: thesis: E . n c= E . m
then ( 0 < n + 1 & n + 1 <= m + 1 ) by XREAL_1:6;
then (b - a) / (m + 1) <= (b - a) / (n + 1) by A3, XREAL_1:118;
then a + ((b - a) / (n + 1)) >= a + ((b - a) / (m + 1)) by XREAL_1:6;
then [.(a + ((b - a) / (n + 1))),b.] c= [.(a + ((b - a) / (m + 1))),b.] by XXREAL_1:34;
then E . n c= [.(a + ((b - a) / (m + 1))),b.] by A2;
hence E . n c= E . m by A2; :: thesis: verum

end;

hence E is non-descending by PROB_1:def 5; :: thesis: ( E is convergent & Union E = ].a,b.] )
hence E is convergent by SETLIM_1:63; :: thesis: Union E = ].a,b.]

now :: thesis: for x being Real st x in Union E holds
x in ].a,b.]

let x be Real; :: thesis: ( x in Union E implies x in ].a,b.] )
assume x in Union E ; :: thesis: x in ].a,b.]
then x in union (rng E) by CARD_3:def 4;
then consider A being set such that
A4: ( x in A & A in rng E ) by TARSKI:def 4;
consider n being Element of NAT such that
A5: A = E . n by A4, FUNCT_2:113;
x in [.(a + ((b - a) / (n + 1))),b.] by A2, A4, A5;
then A6: ( a + ((b - a) / (n + 1)) <= x & x <= b ) by XXREAL_1:1;
a + ((b - a) / (n + 1)) > a by A3, XREAL_1:29;
then x > a by A6, XXREAL_0:2;
hence x in ].a,b.] by A6, XXREAL_1:2; :: thesis: verum

end;

then A7: Union E c= ].a,b.] ;

now :: thesis: for x being Real st x in ].a,b.] holds
x in Union E

let x be Real; :: thesis: ( x in ].a,b.] implies x in Union E )
assume x in ].a,b.] ; :: thesis: x in Union E
then A8: ( a < x & x <= b ) by XXREAL_1:2;
then A9: ( x - a > 0 & b - x >= 0 ) by XREAL_1:48, XREAL_1:50;
consider n being Nat such that
A10: (b - x) / (x - a) < n by SEQ_4:3;
b - x < (x - a) * n by A9, A10, XREAL_1:77;
then (x - a) + (b - x) < (x - a) + ((x - a) * n) by XREAL_1:8;
then b - a < (x - a) * (n + 1) ;
then (b - a) / (n + 1) < x - a by XREAL_1:83;
then x > a + ((b - a) / (n + 1)) by XREAL_1:20;
then x in [.(a + ((b - a) / (n + 1))),b.] by A8, XXREAL_1:1;
then A11: x in E . n by A2;
dom E = NAT by FUNCT_2:def 1;
then E . n in rng E by FUNCT_1:3, ORDINAL1:def 12;
then x in union (rng E) by A11, TARSKI:def 4;
hence x in Union E by CARD_3:def 4; :: thesis: verum

end;

then ].a,b.] c= Union E ;
hence Union E = ].a,b.] by A7, XBOOLE_0:def 10; :: thesis: verum