let X be set ; :: thesis: for S being Field_Subset of X

for M being 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 Field_Subset of X; :: thesis: for M being 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 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 Def4;

then M . (A \ B) <= 0. by Th8, XBOOLE_1:36;

then A4: M . (A \ B) = 0. by A2;

M . B = 0. by Def4;

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, Def4; :: thesis: verum

for M being 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 Field_Subset of X; :: thesis: for M being 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 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 Def4;

then M . (A \ B) <= 0. by Th8, XBOOLE_1:36;

then A4: M . (A \ B) = 0. by A2;

M . B = 0. by Def4;

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, Def4; :: thesis: verum