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 ( W c= A & Z c= X \ A ) ; :: thesis: (C . W) + (C . Z) = C . (W \/ Z)
then ( C . (W \/ Z) <= (C . W) + (C . Z) & (C . W) + (C . Z) <= C . (W \/ Z) ) by A1, Def3, Th12;
hence (C . W) + (C . Z) = C . (W \/ Z) by 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 Def3; :: thesis: verum