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 . (A \/ B) = M . (A \/ (B \ A)) by XBOOLE_1:39
.= (M . A) + (M . (B \ A)) by A1, Def5 ;
A3: B \ A c= B by XBOOLE_1:36;
( 0. <= M . A & 0. <= M . (B \ A) & M . A <= M . A & M . (B \ A) <= M . B ) by A3, Def4, Th25;
hence M . (A \/ B) <= (M . A) + (M . B) by A2, XXREAL_3:38; :: thesis: verum