let A, B, X be set ; :: thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \/ B in sigma_Field C
let C be C_Measure of X; :: thesis: ( A in sigma_Field C & B in sigma_Field C implies A \/ B in sigma_Field C )
assume that
A1: A in sigma_Field C and
A2: B in sigma_Field C ; :: thesis: A \/ B in sigma_Field C
reconsider A = A, B = B as Subset of X by A1, A2;
set D = A \/ B;
for W, Z being Subset of X st W c= A \/ B & Z c= X \ (A \/ B) holds
(C . W) + (C . Z) = C . (W \/ Z)

proof

let W, Z be Subset of X; :: thesis: ( W c= A \/ B & Z c= X \ (A \/ B) implies (C . W) + (C . Z) = C . (W \/ Z) )
assume that
A3: W c= A \/ B and
A4: Z c= X \ (A \/ B) ; :: thesis: (C . W) + (C . Z) = C . (W \/ Z)
set W2 = W \ A;
set Z1 = (W \ A) \/ Z;
A5: (X \ A) /\ (X \ B) c= X \ B by XBOOLE_1:17;
set W1 = W /\ A;
A6: W /\ A c= A by XBOOLE_1:17;
(X \ A) /\ (X \ B) c= X \ A by XBOOLE_1:17;
then A7: X \ (A \/ B) c= X \ A by XBOOLE_1:53;
Z c= (X \ A) /\ (X \ B) by A4, XBOOLE_1:53;
then A8: Z c= X \ B by A5;
W = (W /\ A) \/ (W \ A) by XBOOLE_1:51;
then C . W <= (C . (W /\ A)) + (C . (W \ A)) by Th4;
then A9: (C . W) + (C . Z) <= ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) by XXREAL_3:36;
W \ A c= (B \/ A) \ A by A3, XBOOLE_1:33;
then A10: W \ A c= B \ A by XBOOLE_1:40;
B \ A c= B by XBOOLE_1:36;
then W \ A c= B by A10;
then A11: (C . (W \ A)) + (C . Z) <= C . ((W \ A) \/ Z) by A2, A8, Def2;
C is nonnegative by Def1;
then A12: 0. <= C . (W /\ A) by MEASURE1:def 2;
W \ A c= X \ A by XBOOLE_1:33;
then (W \ A) \/ Z c= (X \ A) \/ Z by XBOOLE_1:9;
then A13: (W \ A) \/ Z c= X \ A by A4, A7, XBOOLE_1:1, XBOOLE_1:12;
C . (W \/ Z) = C . (((W /\ A) \/ (W \ A)) \/ Z) by XBOOLE_1:51
.= C . ((W /\ A) \/ ((W \ A) \/ Z)) by XBOOLE_1:4
.= (C . (W /\ A)) + (C . ((W \ A) \/ Z)) by A1, A6, A13, Th5 ;
then A14: (C . (W /\ A)) + ((C . (W \ A)) + (C . Z)) <= C . (W \/ Z) by A11, XXREAL_3:36;
A15: C is nonnegative by Def1;
then A16: 0. <= C . Z by MEASURE1:def 2;
0. <= C . (W \ A) by A15, MEASURE1:def 2;
then ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) <= C . (W \/ Z) by A16, A12, A14, XXREAL_3:44;
then A17: (C . W) + (C . Z) <= C . (W \/ Z) by A9, XXREAL_0:2;
C . (W \/ Z) <= (C . W) + (C . Z) by Th4;
hence (C . W) + (C . Z) = C . (W \/ Z) by A17, XXREAL_0:1; :: thesis: verum

end;

hence A \/ B in sigma_Field C by Th5; :: thesis: verum