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 Def2;
A2: 0. <= M . (A \ B) by Def2;
A3: M . A = 0. by Def7;
then M . (A \ B) <= 0. by Th8, XBOOLE_1:36;
then A4: M . (A \ B) = 0. by A2;
M . B = 0. by Def7;
then M . (A \/ B) <= 0. + 0. by A3, Th10;
then A5: M . (A \/ B) <= 0. by XXREAL_3:4;
0. <= M . (A \/ B) by Def2;
then A6: M . (A \/ B) = 0. by A5;
M . (A /\ B) <= 0. by A3, Th8, XBOOLE_1:17;
then M . (A /\ B) = 0. by A1;
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, Def7; :: thesis: verum