theorem :: INTEGR22:5

for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for T being Division of A st rho is bounded_variation holds
for F being var_volume of rho,T holds Sum F <= total_vd rho