let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
let M be sigma_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)
M is Measure of S by Th60;
hence M . (A \/ B) <= (M . A) + (M . B) by Th27; :: thesis: verum