theorem Th6: :: MESFUN15:4

for f being PartFunc of REAL,REAL
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)