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 lower_integrable holds
lower_sum (f,D) <= lower_integral f
let D be Division of I; :: thesis: for f being PartFunc of I,REAL st f is lower_integrable holds
lower_sum (f,D) <= lower_integral f
let f be PartFunc of I,REAL; :: thesis: ( f is lower_integrable implies lower_sum (f,D) <= lower_integral f )
assume f is lower_integrable ; :: thesis: lower_sum (f,D) <= lower_integral f
then A1: rng (lower_sum_set f) is bounded_above by INTEGRA1:def 13;
set r = lower_integral f;
lower_integral f = upper_bound (rng (lower_sum_set f)) by INTEGRA1:def 15;
then A2: for s being Real st s in rng (lower_sum_set f) holds
s <= lower_integral f by A1, SEQ_4:def 1;
A3: dom (lower_sum_set f) = divs I by PARTFUN1:def 2;
D in divs I by INTEGRA1:def 3;
then (lower_sum_set f) . D <= lower_integral f by A3, A2, FUNCT_1:3;
hence lower_sum (f,D) <= lower_integral f by INTEGRA1:def 11; :: thesis: verum