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 C in COM Sigma,P

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for C being thin of P holds C in COM Sigma,P

let P be Probability of Sigma; :: thesis: for C being thin of P holds C in COM Sigma,P
let C be thin of P; :: thesis: C in COM Sigma,P
reconsider B = {} as Element of Sigma by PROB_1:42;
B \/ C in COM Sigma,P by Def5;
hence C in COM Sigma,P ; :: thesis: verum