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)

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

hence
A in sigma_Field C
by MEASURE4:def 2; :: thesis: verum
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;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