let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . A <= P . B

let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . A <= P . B

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st A c= B holds

P . A <= P . B

let P be Probability of Sigma; :: thesis: ( A c= B implies P . A <= P . B )

assume A c= B ; :: thesis: P . A <= P . B

then P . (B \ A) = (P . B) - (P . A) by Th33;

then 0 <= (P . B) - (P . A) by Def8;

then 0 + (P . A) <= P . B by XREAL_1:19;

hence P . A <= P . B ; :: thesis: verum

for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . A <= P . B

let Sigma be SigmaField of Omega; :: thesis: for A, B being Event of Sigma

for P being Probability of Sigma st A c= B holds

P . A <= P . B

let A, B be Event of Sigma; :: thesis: for P being Probability of Sigma st A c= B holds

P . A <= P . B

let P be Probability of Sigma; :: thesis: ( A c= B implies P . A <= P . B )

assume A c= B ; :: thesis: P . A <= P . B

then P . (B \ A) = (P . B) - (P . A) by Th33;

then 0 <= (P . B) - (P . A) by Def8;

then 0 + (P . A) <= P . B by XREAL_1:19;

hence P . A <= P . B ; :: thesis: verum