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

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

let x be Real; :: thesis: ( x in Union E implies x in ].-infty,a.] )
assume x in Union E ; :: thesis: x in ].-infty,a.]
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 - n),a.] by A1, A2, A3;
then A4: ( a - n <= x & x <= a ) by XXREAL_1:1;
x in REAL by XREAL_0:def 1;
hence x in ].-infty,a.] by A4, XXREAL_0:12, XXREAL_1:2; :: thesis: verum

end;

then A5: Union E c= ].-infty,a.] ;

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

let x be Real; :: thesis: ( x in ].-infty,a.] implies x in Union E )
assume x in ].-infty,a.] ; :: thesis: x in Union E
then A6: ( -infty < x & x <= a ) by XXREAL_1:2;
consider n being Nat such that
A7: a - x < n by SEQ_4:3;
a - n < x by A7, XREAL_1:11;
then x in [.(a - n),a.] 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 ].-infty,a.] c= Union E ;
hence Union E = ].-infty,a.] by A5, XBOOLE_0:def 10; :: thesis: verum