let X be set ; :: thesis: for A being Subset of X
for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds
A in sigma_Field C
let A be Subset of X; :: thesis: for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds
A in sigma_Field C
let C be C_Measure of X; :: thesis: ( ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) implies A in sigma_Field C )
assume A1: for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ; :: thesis: A in sigma_Field C
for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z)
proof
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)
set Y = W \/ Z;
A4: Z misses A by A3, XBOOLE_1:106;
A5: (W \/ Z) /\ (X \ A) = ((W \/ Z) /\ X) \ A by XBOOLE_1:49
.= ((X /\ W) \/ (X /\ Z)) \ A by XBOOLE_1:23
.= (W \/ (X /\ Z)) \ A by XBOOLE_1:28
.= (W \/ Z) \ A by XBOOLE_1:28
.= (W \ A) \/ (Z \ A) by XBOOLE_1:42
.= {} \/ (Z \ A) by A2, XBOOLE_1:37
.= {} \/ Z by A4, XBOOLE_1:83 ;
(W \/ Z) /\ A = (A /\ W) \/ (A /\ Z) by XBOOLE_1:23
.= W \/ (A /\ Z) by A2, XBOOLE_1:28
.= W \/ {} by A4, XBOOLE_0:def 7 ;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A1, A5; :: thesis: verum
end;
hence A in sigma_Field C by MEASURE4:def 2; :: thesis: verum