let a be Real; :: thesis: for E being sequence of (bool REAL) st ( for n being Nat holds E . n = [.a,(a + n).] ) holds
( E is non-descending & E is convergent & Union E = [.a,+infty.[ )
let E be sequence of (bool REAL); :: thesis: ( ( for n being Nat holds E . n = [.a,(a + n).] ) implies ( E is non-descending & E is convergent & Union E = [.a,+infty.[ ) )
assume A1: for n being Nat holds E . n = [.a,(a + n).] ; :: thesis: ( E is non-descending & E is convergent & Union E = [.a,+infty.[ )
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 a + n <= a + m by XREAL_1:6;
then [.a,(a + n).] c= [.a,(a + m).] by XXREAL_1:34;
then E . n c= [.a,(a + m).] by A1;
hence E . n c= E . m by A1; :: thesis: verum

end;

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

now :: thesis: for x being Real st x in Union E holds
x in [.a,+infty.[

let x be Real; :: thesis: ( x in Union E implies x in [.a,+infty.[ )
assume x in Union E ; :: thesis: x in [.a,+infty.[
then x in union (rng E) by CARD_3:def 4;
then consider A being set such that
A2: ( x in A & A in rng E ) by TARSKI:def 4;
consider n being Element of NAT such that
A3: A = E . n by A2, FUNCT_2:113;
x in [.a,(a + n).] by A1, A2, A3;
then A4: ( a <= x & x <= a + n ) by XXREAL_1:1;
x in REAL by XREAL_0:def 1;
hence x in [.a,+infty.[ by A4, XXREAL_0:9, XXREAL_1:3; :: thesis: verum

end;

then A5: Union E c= [.a,+infty.[ ;

now :: thesis: for x being Real st x in [.a,+infty.[ holds
x in Union E

let x be Real; :: thesis: ( x in [.a,+infty.[ implies x in Union E )
assume x in [.a,+infty.[ ; :: thesis: x in Union E
then A6: ( a <= x & x < +infty ) by XXREAL_1:3;
consider n being Nat such that
A7: x - a < n by SEQ_4:3;
x < a + n by A7, XREAL_1:19;
then x in [.a,(a + n).] by A6, XXREAL_1:1;
then A8: x in E . n by A1;
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 A8, TARSKI:def 4;
hence x in Union E by CARD_3:def 4; :: thesis: verum

end;

then [.a,+infty.[ c= Union E ;
hence Union E = [.a,+infty.[ by A5, XBOOLE_0:def 10; :: thesis: verum