let f be PartFunc of REAL,REAL; :: thesis: for a being Real st f is_right_convergent_in a & f is non-decreasing holds
for x being Real st x in dom f & a < x holds
f . x >= lim_right (f,a)
let a be Real; :: thesis: ( f is_right_convergent_in a & f is non-decreasing implies for x being Real st x in dom f & a < x holds
f . x >= lim_right (f,a) )
assume that
A1: f is_right_convergent_in a and
A2: f is non-decreasing ; :: thesis: for x being Real st x in dom f & a < x holds
f . x >= lim_right (f,a)
let x be Real; :: thesis: ( x in dom f & a < x implies f . x >= lim_right (f,a) )
assume that
A3: x in dom f and
A4: a < x ; :: thesis: f . x >= lim_right (f,a)

hereby :: thesis: verum

assume A5: f . x < lim_right (f,a) ; :: thesis: contradiction
then A6: (lim_right (f,a)) - (f . x) > 0 by XREAL_1:50;
set g1 = (lim_right (f,a)) - (f . x);
consider r being Real such that
A7: a < r and
A8: for r1 being Real st r1 < r & a < r1 & r1 in dom f holds
|.((f . r1) - (lim_right (f,a))).| < (lim_right (f,a)) - (f . x) by A6, A1, LIMFUNC2:42;
consider R being Real such that
A9: ( min (x,r) > R & R > a & R in dom f ) by A1, A4, A7, XXREAL_0:21, LIMFUNC2:def 4;
A10: ( x >= min (x,r) & r >= min (x,r) ) by XXREAL_0:17;
then A11: r > R by A9, XXREAL_0:2;
x > R by A9, A10, XXREAL_0:2;
then A12: f . x >= f . R by A2, A3, A9, RFUNCT_2:def 3;
then lim_right (f,a) > f . R by A5, XXREAL_0:2;
then |.((f . R) - (lim_right (f,a))).| = - ((f . R) - (lim_right (f,a))) by ABSVALUE:def 1, XREAL_1:49;
then (lim_right (f,a)) - (f . R) < (lim_right (f,a)) - (f . x) by A8, A9, A11;
hence contradiction by A12, XREAL_1:10; :: thesis: verum

end;