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 and
A2: C c= A and
A3: P . A = 0 by Def4;
reconsider A = A as Event of Sigma by A1;
A4: (COM P) . A = 0 by A3, Th39;
Sigma c= COM (Sigma,P) by Th28;
then reconsider A = A as Event of COM (Sigma,P) ;
(COM P) . C <= (COM P) . A by A2, PROB_1:34;
hence (COM P) . C = 0 by A4, PROB_1:def 8; :: thesis: verum