let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL
for B being Real st 0 < vol A & ( for D being Division of A
for K being var_volume of rho,D st lower_bound A < D . 1 holds
Sum K <= B ) holds
for D being Division of A
for K being var_volume of rho,D holds Sum K <= B
let rho be Function of A,REAL; :: thesis: for B being Real st 0 < vol A & ( for D being Division of A
for K being var_volume of rho,D st lower_bound A < D . 1 holds
Sum K <= B ) holds
for D being Division of A
for K being var_volume of rho,D holds Sum K <= B
let B be Real; :: thesis: ( 0 < vol A & ( for D being Division of A
for K being var_volume of rho,D st lower_bound A < D . 1 holds
Sum K <= B ) implies for D being Division of A
for K being var_volume of rho,D holds Sum K <= B )
assume A1: 0 < vol A ; :: thesis: ( ex D being Division of A ex K being var_volume of rho,D st
( lower_bound A < D . 1 & not Sum K <= B ) or for D being Division of A
for K being var_volume of rho,D holds Sum K <= B )
assume A2: for D being Division of A
for K being var_volume of rho,D st lower_bound A < D . 1 holds
Sum K <= B ; :: thesis: for D being Division of A
for K being var_volume of rho,D holds Sum K <= B
let D be Division of A; :: thesis: for K being var_volume of rho,D holds Sum K <= B
let K be var_volume of rho,D; :: thesis: Sum K <= B
1 <= len D by FINSEQ_1:20;
then 1 in dom D by FINSEQ_3:25;
then D . 1 in A by INTEGRA1:6;
then lower_bound A <= D . 1 by SEQ_4:def 2;

per cases then ( lower_bound A < D . 1 or lower_bound A = D . 1 ) by XXREAL_0:1;

suppose lower_bound A < D . 1 ; :: thesis: Sum K <= B

hence Sum K <= B by A2; :: thesis: verum

end;

suppose A5: lower_bound A = D . 1 ; :: thesis: Sum K <= B

then reconsider E = D /^ 1 as Division of A by A1, LM95A;
A6: lower_bound A < E . 1 by A1, A5, LM95B;
set L = the var_volume of rho,E;
Sum the var_volume of rho,E <= B by A2, A6;
hence Sum K <= B by A1, A5, LM95C; :: thesis: verum

end;

end;