let a, b be real number ; :: thesis: for s being Real_Sequence
for S being sequence of (Closed-Interval-MSpace a,b) st S = s & a <= b & s is non-increasing holds
S is convergent
let s be Real_Sequence; :: thesis: for S being sequence of (Closed-Interval-MSpace a,b) st S = s & a <= b & s is non-increasing holds
S is convergent
let S be sequence of (Closed-Interval-MSpace a,b); :: thesis: ( S = s & a <= b & s is non-increasing implies S is convergent )
assume A1: ( S = s & a <= b & s is non-increasing ) ; :: thesis: S is convergent
for n being Element of NAT holds s . n > a - 1

proof

let n be Element of NAT ; :: thesis: s . n > a - 1
dom S = NAT by FUNCT_2:def 1;
then A2: s . n in rng S by A1, FUNCT_1:def 5;
the carrier of (Closed-Interval-MSpace a,b) = [.a,b.] by A1, TOPMETR:14;
then A3: ( a <= s . n & s . n <= b ) by A2, XXREAL_1:1;
a < a + 1 by XREAL_1:31;
then a - 1 < a by XREAL_1:21;
hence s . n > a - 1 by A3, XXREAL_0:2; :: thesis: verum

end;

then s is bounded_below by SEQ_2:def 4;
then s is convergent by A1;
hence S is convergent by A1, Th10; :: thesis: verum