let A be non empty closed_interval Subset of REAL; 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; 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; ( 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
; 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; verum