:: deftheorem DeftotalVD defines total_vd INTEGR22:def 4 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL st rho is bounded_variation holds
for b₃ being Real holds
( b₃ = total_vd rho iff ex VD being non empty Subset of REAL st
( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & b₃ = upper_bound VD ) );