theorem Th46: :: COUSIN2:53

for I being non empty closed_interval Subset of REAL
for D being Division of I
for fc being Function of I,REAL st fc = chi (I,I) holds
( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )