theorem Th11: :: MESFUN15:9

for f being PartFunc of REAL,REAL
for a being Real st f is convergent_in+infty & f is non-decreasing holds
for x being Real st x in dom f holds
f . x <= lim_in+infty f