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

hereby :: thesis: ( ( for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) ) implies A in sigma_Field C )

assume A1: A in sigma_Field C ; :: 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
A3: Z c= X \ A ; :: thesis: (C . W) + (C . Z) = C . (W \/ Z)
A4: C . (W \/ Z) <= (C . W) + (C . Z) by Th4;
(C . W) + (C . Z) <= C . (W \/ Z) by A1, A2, A3, Def2;
hence (C . W) + (C . Z) = C . (W \/ Z) by A4, XXREAL_0:1; :: thesis: verum

end;

assume for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) ; :: thesis: A in sigma_Field C
then for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ;
hence A in sigma_Field C by Def2; :: thesis: verum