:: deftheorem Def10 defines lower_sum_set INTEGRA1:def 11 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for b₃ being Function of (divs A),REAL holds
( b₃ = lower_sum_set f iff for D being Division of A holds b₃ . D = lower_sum (f,D) );