let i be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

let D be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

let f be Function of A,REAL; :: thesis: ( f | A is bounded & i in dom D implies upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f) )

assume A1: f | A is bounded ; :: thesis: ( not i in dom D or upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f) )

assume i in dom D ; :: thesis: upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

then divset (D,i) c= A by INTEGRA1:8;

hence upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f) by A1, Lm4; :: thesis: verum

for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A

for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

let D be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded & i in dom D holds

upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

let f be Function of A,REAL; :: thesis: ( f | A is bounded & i in dom D implies upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f) )

assume A1: f | A is bounded ; :: thesis: ( not i in dom D or upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f) )

assume i in dom D ; :: thesis: upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f)

then divset (D,i) c= A by INTEGRA1:8;

hence upper_bound (rng (f | (divset (D,i)))) >= lower_bound (rng f) by A1, Lm4; :: thesis: verum