let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL st rho is bounded_variation holds
0 <= total_vd rho
let rho be Function of A,REAL; :: thesis: ( rho is bounded_variation implies 0 <= total_vd rho )
assume rho is bounded_variation ; :: thesis: 0 <= total_vd rho
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

proof

let p be ExtReal; :: thesis: ( p in VD implies p0 <= p )
assume p in VD ; :: thesis: p0 <= p
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: verum

end;

then p0 is LowerBound of VD by XXREAL_2:def 2;
then B4: VD is bounded_below by XXREAL_2:def 9;
B5: for s being Real st s in VD holds
0 <= s

proof

let s be Real; :: thesis: ( s in VD implies 0 <= s )
assume s in VD ; :: thesis: 0 <= s
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: verum

end;

lower_bound VD <= upper_bound VD by A1, B4, SEQ_4:11;
hence 0 <= total_vd rho by A3, SEQ_4:43, B5; :: thesis: verum