let i be Element of NAT ; :: thesis: for A being 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 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:10;
hence upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f) by A1, Lm4; :: thesis: verum