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)

A5: for n being Element of NAT st n <> 0 holds

(vol (M,Aseq)) . n = 0

(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

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

then reconsider Aseq = Aseq as Covering of A,F by Def3;
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;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

A5: for n being Element of NAT st n <> 0 holds

(vol (M,Aseq)) . n = 0

proof

then
for n being Element of NAT st 1 <= n holds
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;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

(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