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