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 C0: 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
A1: SUM (vol M,G) = r by Def8;
B c= union (rng G) by Def2;
then A c= union (rng G) by C0, XBOOLE_1:1;
then reconsider G1 = G as Covering of A,F by Def2;
SUM (vol M,G) = SUM (vol M,G1) ;
hence r in Svc M,A by A1, Def8; :: thesis: verum

end;

then D1: 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 Def10;
hence (C_Meas M) . A <= (C_Meas M) . B by D1, XXREAL_2:60; :: thesis: verum