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 )
assume A1: f | A is bounded ; :: thesis: lower_sum f,D1 <= upper_sum f,D2
consider D being Division of A such that
A2: ( D1 <= D & D2 <= D ) by Th49;
A3: ( f | A is bounded_below & f | A is bounded_above ) by A1;
then A4: lower_sum f,D1 <= lower_sum f,D by A2, Th48;
A5: lower_sum f,D <= upper_sum f,D by A1, Th30;
upper_sum f,D <= upper_sum f,D2 by A2, A3, Th47;
then lower_sum f,D <= upper_sum f,D2 by A5, XXREAL_0:2;
hence lower_sum f,D1 <= upper_sum f,D2 by A4, XXREAL_0:2; :: thesis: verum