theorem Th39: :: COUSIN2:45

for I being non empty closed_interval Subset of REAL
for TD being tagged_division of I
for f being bounded integrable Function of I,REAL
for i being Nat st i in dom TD holds
( (lower_volume (f,(division_of TD))) . i <= (tagged_volume (f,TD)) . i & (tagged_volume (f,TD)) . i <= (upper_volume (f,(division_of TD))) . i )