for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )