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
() . 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
() . A <= M . A

let M be Measure of F; :: thesis: for A being set st A in F holds
() . A <= M . A

let A9 be set ; :: thesis: ( A9 in F implies () . A9 <= M . A9 )
assume A1: A9 in F ; :: thesis: () . A9 <= M . A9
then reconsider A = A9 as Subset of X ;
reconsider Aseq = (A,({} X)) followed_by ({} X) as Set_Sequence of F by ;
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 ; :: 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 ;
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
.= (vol (M,Aseq)) . 0 by ;
then SUM (vol (M,Aseq)) = M . (Aseq . 0) by Def5;
then A6: M . A in Svc (M,A) by ;
(C_Meas M) . A = inf (Svc (M,A)) by Def8;
hence (C_Meas M) . A9 <= M . A9 by ; :: thesis: verum