let a, b be Real_Sequence; :: thesis: ( ( for n being Nat holds a . n <= b . n ) & b is convergent & a is non-decreasing implies ( a is convergent & lim a <= lim b ) )
assume that
A1: for n being Nat holds a . n <= b . n and
A2: b is convergent and
A3: a is non-decreasing ; :: thesis: ( a is convergent & lim a <= lim b )
A4: b is bounded by A2;
A5: a is bounded_above

proof

consider r being Real such that
A6: for n being Nat holds b . n < r by A4, SEQ_2:def 3;

now :: thesis: for n being Nat holds a . n < r + 1

let n be Nat; :: thesis: a . n < r + 1
a . n <= b . n by A1;
then a . n <= r by A6, XXREAL_0:2;
then (a . n) + 0 < r + 1 by XREAL_1:8;
hence a . n < r + 1 ; :: thesis: verum

end;

hence a is bounded_above by SEQ_2:def 3; :: thesis: verum

end;

hence a is convergent by A3; :: thesis: lim a <= lim b
thus lim a <= lim b by A1, A2, A3, A5, SEQ_2:18; :: thesis: verum