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

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