theorem Th9: :: MESFUN15:7

for f being PartFunc of REAL,REAL
for a being Real st f is_right_convergent_in a & f is non-increasing holds
for x being Real st x in dom f & a < x holds
f . x <= lim_right (f,a)