let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds Sigma c= COM Sigma,P
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma holds Sigma c= COM Sigma,P
let P be Probability of Sigma; :: thesis: Sigma c= COM Sigma,P
let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in Sigma or A in COM Sigma,P )
assume A1: A in Sigma ; :: thesis: A in COM Sigma,P
reconsider C = {} as thin of P by Th25;
A = A \/ C ;
hence A in COM Sigma,P by A1, Def5; :: thesis: verum