set VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } ;
set t0 = the Division of A;
set F0 = the var_volume of rho, the Division of A;
A11: Sum the var_volume of rho, the Division of A in { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } ;
for z being object st z in { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } holds
z in REAL

proof

let z be object ; :: thesis: ( z in { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } implies z in REAL )
assume z in { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } ; :: thesis: z in REAL
then consider r being Real such that
A2: ( z = r & ex t being Division of A ex F being var_volume of rho,t st r = Sum F ) ;
thus z in REAL by A2, XREAL_0:def 1; :: thesis: verum

end;

then reconsider VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } as non empty Subset of REAL by A11, TARSKI:def 3;
consider d being Real such that
A3: ( 0 <= d & ( for t being Division of A
for F being var_volume of rho,t holds Sum F <= d ) ) by AS;
for p being ExtReal st p in VD holds
p <= d

proof

let p be ExtReal; :: thesis: ( p in VD implies p <= d )
assume p in VD ; :: thesis: p <= d
then consider r being Real such that
A4: ( p = r & ex t being Division of A ex F being var_volume of rho,t st r = Sum F ) ;
consider t being Division of A, F being var_volume of rho,t such that
A5: r = Sum F by A4;
Sum F <= d by A3;
hence p <= d by A4, A5; :: thesis: verum

end;

then d is UpperBound of VD by XXREAL_2:def 1;
then B1: VD is bounded_above by XXREAL_2:def 10;
set z = upper_bound VD;
take upper_bound VD ; :: thesis: ex VD being non empty Subset of REAL st
( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & upper_bound VD = upper_bound VD )
thus ex VD being non empty Subset of REAL st
( VD is bounded_above & VD = { r where r is Real : ex t being Division of A ex F being var_volume of rho,t st r = Sum F } & upper_bound VD = upper_bound VD ) by B1; :: thesis: verum