let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded holds
for D, D1 being Division of A ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) )
let f be Function of A,REAL; :: thesis: ( f | A is bounded implies for D, D1 being Division of A ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) ) )
assume A1: f | A is bounded ; :: thesis: for D, D1 being Division of A ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) )
let D, D1 be Division of A; :: thesis: ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) )
consider D2 being Division of A such that
A3: D <= D2 and
A4: D1 <= D2 and
A5: rng D2 = (rng D1) \/ (rng D) by Th4;
A6: (upper_sum (f,D1)) - (upper_sum (f,D2)) >= 0 by A1, A4, INTEGRA1:45, XREAL_1:48;
(upper_sum (f,D)) - (upper_sum (f,D2)) >= 0 by A1, A3, INTEGRA1:45, XREAL_1:48;
hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) ) by A3, A4, A5, A6; :: thesis: verum