theorem Th54: :: INTEGRA1:56

for A being non empty closed_interval Subset of REAL
for D being Division of A
for f, g being Function of A,REAL st f | A is bounded_below & g | A is bounded_below holds
(lower_sum (f,D)) + (lower_sum (g,D)) <= lower_sum ((f + g),D)