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

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