let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A
for f being Function of A,REAL st f | A is bounded holds
lower_sum (f,D1) <= upper_sum (f,D2)
let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded holds
lower_sum (f,D1) <= upper_sum (f,D2)
let f be Function of A,REAL; :: thesis: ( f | A is bounded implies lower_sum (f,D1) <= upper_sum (f,D2) )
consider D being Division of A such that
A1: D1 <= D and
A2: D2 <= D by Th45;
assume A3: f | A is bounded ; :: thesis: lower_sum (f,D1) <= upper_sum (f,D2)
then A4: lower_sum (f,D) <= upper_sum (f,D) by Th26;
upper_sum (f,D) <= upper_sum (f,D2) by A3, A2, Th43;
then A5: lower_sum (f,D) <= upper_sum (f,D2) by A4, XXREAL_0:2;
lower_sum (f,D1) <= lower_sum (f,D) by A3, A1, Th44;
hence lower_sum (f,D1) <= upper_sum (f,D2) by A5, XXREAL_0:2; :: thesis: verum