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, 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 A2, PROB_1:70;
hence (COM P) . C = 0 by A4, PROB_1:def 13; :: thesis: verum