let I be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of I,REAL st f is upper_integrable holds
ex r being Real st
for D being Division of I holds r < upper_sum (f,D)
let f be PartFunc of I,REAL; :: thesis: ( f is upper_integrable implies ex r being Real st
for D being Division of I holds r < upper_sum (f,D) )
assume f is upper_integrable ; :: thesis: ex r being Real st
for D being Division of I holds r < upper_sum (f,D)
then rng (upper_sum_set f) is bounded_below by INTEGRA1:def 12;
then consider r being Real such that
A1: for y being object st y in dom (upper_sum_set f) holds
r < (upper_sum_set f) . y by INTEGRA1:12, SEQ_2:def 2;
A2: dom (upper_sum_set f) = divs I by FUNCT_2:def 1;
take r ; :: thesis: for D being Division of I holds r < upper_sum (f,D)
let D be Division of I; :: thesis: r < upper_sum (f,D)
D in divs I by INTEGRA1:def 3;
then r < (upper_sum_set f) . D by A1, A2;
hence r < upper_sum (f,D) by INTEGRA1:def 10; :: thesis: verum