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

hereby :: thesis: verum

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

end;