:: deftheorem defines lower_integral INTEGRA1:def 15 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL holds lower_integral f = upper_bound (rng (lower_sum_set f));