:: deftheorem Def9 defines upper_sum_set INTEGRA1:def 10 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for b₃ being Function of (divs A),REAL holds
( b₃ = upper_sum_set f iff for D being Division of A holds b₃ . D = upper_sum (f,D) );