let A, X be set ; :: thesis: for C being C_Measure of X st A in sigma_Field C holds
X \ A in sigma_Field C
let C be C_Measure of X; :: thesis: ( A in sigma_Field C implies X \ A in sigma_Field C )
assume A1: A in sigma_Field C ; :: thesis: X \ A in sigma_Field C
for W, Z being Subset of X st W c= X \ A & Z c= X \ (X \ A) holds
(C . W) + (C . Z) <= C . (W \/ Z)

proof

let W, Z be Subset of X; :: thesis: ( W c= X \ A & Z c= X \ (X \ A) implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A2: W c= X \ A and
A3: Z c= X \ (X \ A) ; :: thesis: (C . W) + (C . Z) <= C . (W \/ Z)
X \ (X \ A) = X /\ A by XBOOLE_1:48;
then Z c= A by A1, A3, XBOOLE_1:28;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A1, A2, Def2; :: thesis: verum

end;

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