theorem Th52: :: INTEGRA1:54

for i being Element of NAT
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 i in dom D & f | A is bounded_below & g | A is bounded_below holds
((lower_volume (f,D)) . i) + ((lower_volume (g,D)) . i) <= (lower_volume ((f + g),D)) . i