:: deftheorem defines upper_integral INTEGRA1:def 14 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL holds upper_integral f = lower_bound (rng (upper_sum_set f));