let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let F be Field_Subset of X; :: thesis: for M being Measure of F

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let M be Measure of F; :: thesis: for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let Sets be SetSequence of X; :: thesis: for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let Cvr be Covering of Sets,F; :: thesis: inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

set Q = SUM (vol (M,(On Cvr)));

for x being ExtReal st x in rng (Ser (vol (M,(On Cvr)))) holds

ex y being ExtReal st

( y in rng (Ser (Volume (M,Cvr))) & x <= y )

SUM (vol (M,(On Cvr))) in Svc (M,(union (rng Sets))) by Def7;

then inf (Svc (M,(union (rng Sets)))) <= SUM (vol (M,(On Cvr))) by XXREAL_2:3;

hence inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) by A4, XXREAL_0:2; :: thesis: verum

for M being Measure of F

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let F be Field_Subset of X; :: thesis: for M being Measure of F

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let M be Measure of F; :: thesis: for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let Sets be SetSequence of X; :: thesis: for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

let Cvr be Covering of Sets,F; :: thesis: inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

set Q = SUM (vol (M,(On Cvr)));

for x being ExtReal st x in rng (Ser (vol (M,(On Cvr)))) holds

ex y being ExtReal st

( y in rng (Ser (Volume (M,Cvr))) & x <= y )

proof

then A4:
SUM (vol (M,(On Cvr))) <= SUM (Volume (M,Cvr))
by XXREAL_2:63;
let x be ExtReal; :: thesis: ( x in rng (Ser (vol (M,(On Cvr)))) implies ex y being ExtReal st

( y in rng (Ser (Volume (M,Cvr))) & x <= y ) )

assume x in rng (Ser (vol (M,(On Cvr)))) ; :: thesis: ex y being ExtReal st

( y in rng (Ser (Volume (M,Cvr))) & x <= y )

then consider n being Element of NAT such that

A1: x = (Ser (vol (M,(On Cvr)))) . n by FUNCT_2:113;

consider m being Nat such that

A2: for Sets being SetSequence of X

for G being Covering of Sets,F holds (Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th6;

take (Ser (Volume (M,Cvr))) . m ; :: thesis: ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m )

A3: for Sets being SetSequence of X

for G being Covering of Sets,F holds (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m

hence ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m ) by A1, A3, FUNCT_2:4; :: thesis: verum

end;( y in rng (Ser (Volume (M,Cvr))) & x <= y ) )

assume x in rng (Ser (vol (M,(On Cvr)))) ; :: thesis: ex y being ExtReal st

( y in rng (Ser (Volume (M,Cvr))) & x <= y )

then consider n being Element of NAT such that

A1: x = (Ser (vol (M,(On Cvr)))) . n by FUNCT_2:113;

consider m being Nat such that

A2: for Sets being SetSequence of X

for G being Covering of Sets,F holds (Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th6;

take (Ser (Volume (M,Cvr))) . m ; :: thesis: ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m )

A3: for Sets being SetSequence of X

for G being Covering of Sets,F holds (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m

proof

m in NAT
by ORDINAL1:def 12;
let Sets be SetSequence of X; :: thesis: for G being Covering of Sets,F holds (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m

let G be Covering of Sets,F; :: thesis: (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m

(Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by A2;

then (Ser (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th1;

hence (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m by Th1; :: thesis: verum

end;let G be Covering of Sets,F; :: thesis: (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m

(Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by A2;

then (Ser (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th1;

hence (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m by Th1; :: thesis: verum

hence ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m ) by A1, A3, FUNCT_2:4; :: thesis: verum

SUM (vol (M,(On Cvr))) in Svc (M,(union (rng Sets))) by Def7;

then inf (Svc (M,(union (rng Sets)))) <= SUM (vol (M,(On Cvr))) by XXREAL_2:3;

hence inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) by A4, XXREAL_0:2; :: thesis: verum