let A be non empty closed_interval Subset of REAL; :: thesis:
let rho be Function of A,REAL; :: thesis:
assume rho is bounded_variation ; :: thesis:
then consider VD being non empty Subset of REAL such that
A1: VD is bounded_above and
A2: VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } and
A3: total_vd rho = upper_bound VD by DeftotalVD;
reconsider p0 = 0 as Real ;
for p being ExtReal st p in VD holds
p0 <= p

let p be ExtReal; :: thesis:
assume p in VD ; :: thesis:
then consider r being Real such that
B1: p = r and
B2: ex t being Division of A ex F being var_volume of rho,t st r = Sum F by A2;
ex t being Division of A ex F being var_volume of rho,t st r = Sum F by B2;
hence p0 <= p by B1, LM2; :: thesis:

end;

let s be Real; :: thesis:
assume s in VD ; :: thesis:
then consider r being Real such that
B1: s = r and
B2: ex t being Division of A ex F being var_volume of rho,t st r = Sum F by A2;
ex t being Division of A ex F being var_volume of rho,t st r = Sum F by B2;
hence 0 <= s by B1, LM2; :: thesis:

end;