theorem Th40: :: COUSIN2:46

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 holds
( Sum (lower_volume (f,(division_of TD))) <= Sum (tagged_volume (f,TD)) & Sum (tagged_volume (f,TD)) <= Sum (upper_volume (f,(division_of TD))) )