let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for A, B being Subset of X st A c= B holds
(C_Meas M) . A <= (C_Meas M) . B
let F be Field_Subset of X; :: thesis: for M being Measure of F
for A, B being Subset of X st A c= B holds
(C_Meas M) . A <= (C_Meas M) . B
let M be Measure of F; :: thesis: for A, B being Subset of X st A c= B holds
(C_Meas M) . A <= (C_Meas M) . B
let A, B be Subset of X; :: thesis: ( A c= B implies (C_Meas M) . A <= (C_Meas M) . B )
assume A1: A c= B ; :: thesis: (C_Meas M) . A <= (C_Meas M) . B

now

let r be set ; :: thesis: ( r in Svc (M,B) implies r in Svc (M,A) )
assume r in Svc (M,B) ; :: thesis: r in Svc (M,A)
then consider G being Covering of B,F such that
A2: SUM (vol (M,G)) = r by Def7;
B c= union (rng G) by Def3;
then A c= union (rng G) by A1, XBOOLE_1:1;
then reconsider G1 = G as Covering of A,F by Def3;
SUM (vol (M,G)) = SUM (vol (M,G1)) ;
hence r in Svc (M,A) by A2, Def7; :: thesis: verum

end;

then A3: Svc (M,B) c= Svc (M,A) by TARSKI:def 3;
( (C_Meas M) . A = inf (Svc (M,A)) & (C_Meas M) . B = inf (Svc (M,B)) ) by Def8;
hence (C_Meas M) . A <= (C_Meas M) . B by A3, XXREAL_2:60; :: thesis: verum