theorem Th5: :: INTEGRA3:5

for A being non empty closed_interval Subset of REAL
for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds
for x, y being Real
for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) holds
x = y