let I be non empty closed_interval Subset of REAL; :: thesis: for D being Division of I
for f being PartFunc of I,REAL st f is upper_integrable holds
upper_integral f <= upper_sum (f,D)
let D be Division of I; :: thesis: for f being PartFunc of I,REAL st f is upper_integrable holds
upper_integral f <= upper_sum (f,D)
let f be PartFunc of I,REAL; :: thesis: ( f is upper_integrable implies upper_integral f <= upper_sum (f,D) )
assume f is upper_integrable ; :: thesis: upper_integral f <= upper_sum (f,D)
then A1: rng (upper_sum_set f) is bounded_below by INTEGRA1:def 12;
set r = upper_integral f;
upper_integral f = lower_bound (rng (upper_sum_set f)) by INTEGRA1:def 14;
then A2: for s being Real st s in rng (upper_sum_set f) holds
upper_integral f <= s by A1, SEQ_4:def 2;
A3: dom (upper_sum_set f) = divs I by PARTFUN1:def 2;
D in divs I by INTEGRA1:def 3;
then upper_integral f <= (upper_sum_set f) . D by A3, A2, FUNCT_1:3;
hence upper_integral f <= upper_sum (f,D) by INTEGRA1:def 10; :: thesis: verum