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 st A c= B holds
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 st A c= B holds
M . A <= M . B
let M be 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 )
reconsider C = B \ A as Element of S ;
A1: 0. <= M . C by Def2;
A misses C by XBOOLE_1:79;
then A2: M . (A \/ C) = (M . A) + (M . C) by Def3;
assume A c= B ; :: thesis: M . A <= M . B
then M . B = (M . A) + (M . C) by A2, XBOOLE_1:45;
hence M . A <= M . B by A1, XXREAL_3:39; :: thesis: verum