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)
reconsider C = {} as thin of P by Th24;
let A be object ; :: 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 AA = A as set by TARSKI:1;
A = AA \/ C ;
hence A in COM (Sigma,P) by A1, Def5; :: thesis: verum