theorem Th18: :: COUSIN2:21

for I being non empty closed_interval Subset of REAL
for D being Division of I
for f being PartFunc of I,REAL st f is lower_integrable holds
lower_sum (f,D) <= lower_integral f