let A be 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 Th49;
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 Th30;
upper_sum f,D <= upper_sum f,D2 by A3, A2, Th47;
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, Th48;
hence lower_sum f,D1 <= upper_sum f,D2 by A5, XXREAL_0:2; :: thesis: verum