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 )

proof

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

proof

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;

m in NAT by ORDINAL1:def 12;
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;

then A4: SUM (vol (M,(On Cvr))) <= SUM (Volume (M,Cvr)) by XXREAL_2:63;
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