let X be set ; :: thesis: for C being C_Measure of X
for A being Subset of X st C . A = 0. holds
A in sigma_Field C
let C be C_Measure of X; :: thesis: for A being Subset of X st C . A = 0. holds
A in sigma_Field C
let A be Subset of X; :: thesis: ( C . A = 0. implies A in sigma_Field C )
assume A1: C . A = 0. ; :: thesis: A in sigma_Field C

now :: thesis: for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z)

let W, Z be Subset of X; :: thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A2: W c= A and
Z c= X \ A ; :: thesis: (C . W) + (C . Z) <= C . (W \/ Z)
Z c= W \/ Z by XBOOLE_1:7;
then A3: C . Z <= C . (W \/ Z) by Def1;
C is nonnegative by Def1;
then 0. <= C . W by MEASURE1:def 2;
then C . W = 0. by A1, A2, Def1;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A3, XXREAL_3:4; :: thesis: verum

end;

hence A in sigma_Field C by Def2; :: thesis: verum