let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
let P be Probability of Sigma; :: thesis: for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
let A, B be Event of Sigma; :: thesis: ( A c= B & P . B = 0 implies P . A = 0 )
assume ( A c= B & P . B = 0 ) ; :: thesis: P . A = 0
then P . A <= 0 by PROB_1:34;
hence P . A = 0 by PROB_1:def 8; :: thesis: verum