:: deftheorem defines upper_integrable INTEGRA1:def 12 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL holds
( f is upper_integrable iff rng (upper_sum_set f) is bounded_below );