for A being non empty closed_interval Subset of REAL
for D1 being Division of A
for f being Function of A,REAL
for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
( ( for i being Element of NAT st i in Seg (len D1) holds
divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )