let I be non empty closed_interval Subset of REAL; :: thesis: 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
let f be PartFunc of I,REAL; :: thesis: ( f is lower_integrable implies ex r being Real st
for D being Division of I holds lower_sum (f,D) < r )
assume f is lower_integrable ; :: thesis: ex r being Real st
for D being Division of I holds lower_sum (f,D) < r
then rng (lower_sum_set f) is bounded_above by INTEGRA1:def 13;
then consider r being Real such that
A1: for y being object st y in dom (lower_sum_set f) holds
(lower_sum_set f) . y < r by INTEGRA1:14, SEQ_2:def 1;
A2: dom (lower_sum_set f) = divs I by FUNCT_2:def 1;
take r ; :: thesis: for D being Division of I holds lower_sum (f,D) < r
let D be Division of I; :: thesis: lower_sum (f,D) < r
D in divs I by INTEGRA1:def 3;
then (lower_sum_set f) . D < r by A1, A2;
hence lower_sum (f,D) < r by INTEGRA1:def 11; :: thesis: verum