:: deftheorem defines upper_sum INTEGRA1:def 8 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A holds upper_sum (f,D) = Sum (upper_volume (f,D));