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 st A c= B holds
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 st A c= B holds
M . A <= M . B
let M be sigma_Measure of S; :: thesis: for A, B being Element of S st A c= B holds
M . A <= M . B
let A, B be Element of S; :: thesis: ( A c= B implies M . A <= M . B )
assume A1: A c= B ; :: thesis: M . A <= M . B
M is Measure of S by Th60;
hence M . A <= M . B by A1, Th25; :: thesis: verum