for I being non empty closed_interval Subset of REAL
for f being Function of I,REAL
for D, D1 being Division of I st D . 1 = lower_bound I & D1 = D /^ 1 holds
( upper_sum (f,D1) = upper_sum (f,D) & lower_sum (f,D1) = lower_sum (f,D) )