let X, A, B 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 A1: ( A in sigma_Field C & B in sigma_Field C ) ; :: thesis: A \/ B in sigma_Field C
then reconsider A = A, B = B as Subset of X ;
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 A2: ( W c= A \/ B & Z c= X \ (A \/ B) ) ; :: thesis: (C . W) + (C . Z) = C . (W \/ Z)
set W1 = W /\ A;
A3: W \ A c= X \ A by XBOOLE_1:33;
set W2 = W \ A;
(X \ A) /\ (X \ B) c= X \ A by XBOOLE_1:17;
then B4: X \ (A \/ B) c= X \ A by XBOOLE_1:53;
then A4: ( W /\ A c= A & Z c= X \ A ) by A2, XBOOLE_1:1, XBOOLE_1:17;
A5: (W \ A) \/ Z c= (X \ A) \/ Z by A3, XBOOLE_1:9;
set Z1 = (W \ A) \/ Z;
A6: (W \ A) \/ Z c= X \ A by B4, A5, A2, XBOOLE_1:1, XBOOLE_1:12;
A7: W = (W /\ A) \/ (W \ A) by XBOOLE_1:51;
A8: 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, A4, A6, Th14 ;
W \ A c= (B \/ A) \ A by A2, XBOOLE_1:33;
then ( W \ A c= B \ A & B \ A c= B ) by XBOOLE_1:36, XBOOLE_1:40;
then A9: W \ A c= B by XBOOLE_1:1;
( Z c= (X \ A) /\ (X \ B) & (X \ A) /\ (X \ B) c= X \ B ) by A2, XBOOLE_1:17, XBOOLE_1:53;
then Z c= X \ B by XBOOLE_1:1;
then A10: (C . (W \ A)) + (C . Z) <= C . ((W \ A) \/ Z) by A1, A9, Def3;
C is nonnegative by Def2;
then A11: ( 0. <= C . (W \ A) & 0. <= C . Z ) by MEASURE1:def 4;
C is nonnegative by Def2;
then A13: 0. <= C . (W /\ A) by MEASURE1:def 4;
(C . (W /\ A)) + ((C . (W \ A)) + (C . Z)) <= C . (W \/ Z) by A8, A10, XXREAL_3:38;
then A14: ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) <= C . (W \/ Z) by A11, A13, XXREAL_3:48;
C . W <= (C . (W /\ A)) + (C . (W \ A)) by A7, Th12;
then (C . W) + (C . Z) <= ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) by XXREAL_3:38;
then A16: (C . W) + (C . Z) <= C . (W \/ Z) by A14, XXREAL_0:2;
C . (W \/ Z) <= (C . W) + (C . Z) by Th12;
hence (C . W) + (C . Z) = C . (W \/ Z) by A16, XXREAL_0:1; :: thesis: verum

end;

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