for I being non empty closed_interval Subset of REAL
for D being Division of I
for f being PartFunc of I,REAL st f is upper_integrable holds
upper_integral f <= upper_sum (f,D)