for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f | A is bounded holds
( f is upper_integrable & f is lower_integrable )