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:123;
A3: Aseq . 0 = A by FUNCT_7:122;
A c= union (rng Aseq)

proof

let x be object ; :: 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:3;
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:124, NAT_1:25;
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:48
.= (vol (M,Aseq)) . 0 by A5, MEASURE7:9 ;
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