theorem Th18: :: INTEGRA1:20

for i being Element of NAT
for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D holds
vol (divset (D,i)) = (upper_volume ((chi (A,A)),D)) . i