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

for M being Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

let S be Field_Subset of X; :: thesis: for M being Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

let M be Measure of S; :: thesis: for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

let A, B be Element of S; :: thesis: M . (A \/ B) <= (M . A) + (M . B)

set C = B \ A;

A1: A misses B \ A by XBOOLE_1:79;

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

M . (A \/ B) = M . (A \/ (B \ A)) by XBOOLE_1:39

.= (M . A) + (M . (B \ A)) by A1, Def3 ;

hence M . (A \/ B) <= (M . A) + (M . B) by A2, XXREAL_3:36; :: thesis: verum

for M being Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

let S be Field_Subset of X; :: thesis: for M being Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

let M be Measure of S; :: thesis: for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

let A, B be Element of S; :: thesis: M . (A \/ B) <= (M . A) + (M . B)

set C = B \ A;

A1: A misses B \ A by XBOOLE_1:79;

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

M . (A \/ B) = M . (A \/ (B \ A)) by XBOOLE_1:39

.= (M . A) + (M . (B \ A)) by A1, Def3 ;

hence M . (A \/ B) <= (M . A) + (M . B) by A2, XXREAL_3:36; :: thesis: verum