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 ext-real number st x in rng (Ser (vol M,(On Cvr))) holds
ex y being ext-real number st
( y in rng (Ser (Volume M,Cvr)) & x <= y )

proof

let x be ext-real number ; :: thesis: ( x in rng (Ser (vol M,(On Cvr))) implies ex y being ext-real number st
( y in rng (Ser (Volume M,Cvr)) & x <= y ) )
assume x in rng (Ser (vol M,(On Cvr))) ; :: thesis: ex y being ext-real number 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:190;
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 13;
hence ( (Ser (Volume M,Cvr)) . m in rng (Ser (Volume M,Cvr)) & x <= (Ser (Volume M,Cvr)) . m ) by A1, A3, FUNCT_2:6; :: 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