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

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

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

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

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;
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;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

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

then
d is UpperBound of VD
by XXREAL_2:def 1;
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;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

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