let A, B, X be set ; 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; ( 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
; 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;
( 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)
;
(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
V92()
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
V92()
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;
verum
end;
hence
A \/ B in sigma_Field C
by Th5; verum