let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds (COM P) . C = 0
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for C being thin of P holds (COM P) . C = 0
let P be Probability of Sigma; :: thesis: for C being thin of P holds (COM P) . C = 0
let C be thin of P; :: thesis: (COM P) . C = 0
consider A being set such that
A1: ( A in Sigma & C c= A & P . A = 0 ) by Def4;
reconsider A = A as Event of Sigma by A1;
A2: (COM P) . A = 0 by A1, Th40;
Sigma c= COM Sigma,P by Th29;
then reconsider A = A as Event of COM Sigma,P by A1;
(COM P) . C <= (COM P) . A by A1, PROB_1:70;
hence (COM P) . C = 0 by A2, PROB_1:def 13; :: thesis: verum