let X be set ; 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; 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; 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; ( A c= B implies (C_Meas M) . A <= (C_Meas M) . B )
assume A1:
A c= B
; (C_Meas M) . A <= (C_Meas M) . B
now for r being object st r in Svc (M,B) holds
r in Svc (M,A)let r be
object ;
( r in Svc (M,B) implies r in Svc (M,A) )assume
r in Svc (
M,
B)
;
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;
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; verum