theorem :: INTEGRA5:16

for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is monotone & A c= dom f holds
f is_integrable_on A