let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for A being set st A in F holds
(C_Meas M) . A <= M . A
let F be Field_Subset of X; :: thesis: for M being Measure of F
for A being set st A in F holds
(C_Meas M) . A <= M . A
let M be Measure of F; :: thesis: for A being set st A in F holds
(C_Meas M) . A <= M . A
let A9 be set ; :: thesis: ( A9 in F implies (C_Meas M) . A9 <= M . A9 )
assume A1: A9 in F ; :: thesis: (C_Meas M) . A9 <= M . A9
then reconsider A = A9 as Subset of X ;
reconsider Aseq = A,({} X) followed_by ({} X) as Set_Sequence of F by A1, Th8;
A2: Aseq . 1 = {} X by FUNCT_7:125;
A3: Aseq . 0 = A by FUNCT_7:124;
A c= union (rng Aseq)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union (rng Aseq) )
dom Aseq = NAT by FUNCT_2:def 1;
then A4: Aseq . 0 in rng Aseq by FUNCT_1:12;
assume x in A ; :: thesis: x in union (rng Aseq)
hence x in union (rng Aseq) by A3, A4, TARSKI:def 4; :: thesis: verum

end;

then reconsider Aseq = Aseq as Covering of A,F by Def3;
A5: for n being Element of NAT st n <> 0 holds
(vol M,Aseq) . n = 0

proof

let n be Element of NAT ; :: thesis: ( n <> 0 implies (vol M,Aseq) . n = 0 )
assume n <> 0 ; :: thesis: (vol M,Aseq) . n = 0
then Aseq . n = {} by A2, FUNCT_7:126, NAT_1:26;
then (vol M,Aseq) . n = M . {} by Def5;
hence (vol M,Aseq) . n = 0 by VALUED_0:def 19; :: thesis: verum

end;

then for n being Element of NAT st 1 <= n holds
(vol M,Aseq) . n = 0 ;
then SUM (vol M,Aseq) = (Ser (vol M,Aseq)) . 1 by Th4, SUPINF_2:67
.= (vol M,Aseq) . 0 by A5, MEASURE7:10 ;
then SUM (vol M,Aseq) = M . (Aseq . 0 ) by Def5;
then A6: M . A in Svc M,A by A3, Def7;
(C_Meas M) . A = inf (Svc M,A) by Def8;
hence (C_Meas M) . A9 <= M . A9 by A6, XXREAL_2:3; :: thesis: verum