let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let M be sigma_Measure of S; :: thesis: for A, B being measure_zero of M holds
( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
let A, B be measure_zero of M; :: thesis: ( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )
A1: 0. <= M . (A /\ B) by Def4;
A2: 0. <= M . (A \ B) by Def4;
A3: M . A = 0. by Def13;
then M . (A \ B) <= 0. by Th62, XBOOLE_1:36;
then A4: M . (A \ B) = 0. by A2, XXREAL_0:1;
M . B = 0. by Def13;
then M . (A \/ B) <= 0. + 0. by A3, Th64;
then A5: M . (A \/ B) <= 0. by XXREAL_3:4;
0. <= M . (A \/ B) by Def4;
then A6: M . (A \/ B) = 0. by A5, XXREAL_0:1;
M . (A /\ B) <= 0. by A3, Th62, XBOOLE_1:17;
then M . (A /\ B) = 0. by A1, XXREAL_0:1;
hence ( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M ) by A6, A4, Def13; :: thesis: verum