:: deftheorem Def6 defines integral INTEGR22:def 9 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u is_RiemannStieltjes_integrable_with rho holds
for b₄ being Real holds
( b₄ = integral (u,rho) iff for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum S is convergent & lim (middle_sum S) = b₄ ) );