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