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

( (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

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)

then A3:
Svc (M,B) c= Svc (M,A)
;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;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

( (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