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