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:4;
B \/ C in COM (Sigma,P) by Def5;
hence C in COM (Sigma,P) ; :: thesis: verum