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 :: thesis: for r being object st r in Svc (M,B) holds
r in Svc (M,A)

let r be object ; :: 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;
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) ;
( (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