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 - ((b - a) / (n + 1))).] ) 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 - ((b - a) / (n + 1))).] ) 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 - ((b - a) / (n + 1))).] ; :: 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 b - ((b - a) / (n + 1)) <= b - ((b - a) / (m + 1)) by XREAL_1:10;
then [.a,(b - ((b - a) / (n + 1))).] c= [.a,(b - ((b - a) / (m + 1))).] by XXREAL_1:34;
then E . n c= [.a,(b - ((b - a) / (m + 1))).] 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 - ((b - a) / (n + 1))).] by A2, A4, A5;
then A6: ( a <= x & x <= b - ((b - a) / (n + 1)) ) by XXREAL_1:1;
b - ((b - a) / (n + 1)) < b by A3, XREAL_1:44;
then x < b by A6, XXREAL_0:2;
hence x in [.a,b.[ by A6, XXREAL_1:3; :: 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:3;
then A9: ( x - a >= 0 & b - x > 0 ) by XREAL_1:48, XREAL_1:50;
consider n being Nat such that
A10: (x - a) / (b - x) < n by SEQ_4:3;
x - a < (b - x) * n by A9, A10, XREAL_1:77;
then (b - x) + (x - a) < (b - x) + ((b - x) * n) by XREAL_1:8;
then b - a < (b - x) * (n + 1) ;
then (b - a) / (n + 1) < b - x by XREAL_1:83;
then x < b - ((b - a) / (n + 1)) by XREAL_1:12;
then x in [.a,(b - ((b - a) / (n + 1))).] 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