let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P))
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P))
let P be Probability of Sigma; :: thesis: COM (Sigma,P) = COM (Sigma,(P2M P))
A1: COM (Sigma,(P2M P)) c= COM (Sigma,P)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COM (Sigma,(P2M P)) or x in COM (Sigma,P) )
assume x in COM (Sigma,(P2M P)) ; :: thesis: x in COM (Sigma,P)
then consider B being set such that
A2: B in Sigma and
A3: ex C being thin of P2M P st x = B \/ C by MEASURE3:def 3;
consider C being thin of P2M P such that
A4: x = B \/ C by A3;
reconsider C1 = C as thin of P by Th23;
x = B \/ C1 by A4;
hence x in COM (Sigma,P) by A2, Def5; :: thesis: verum

end;

COM (Sigma,P) c= COM (Sigma,(P2M P))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in COM (Sigma,P) or x in COM (Sigma,(P2M P)) )
assume x in COM (Sigma,P) ; :: thesis: x in COM (Sigma,(P2M P))
then consider B being set such that
A5: B in Sigma and
A6: ex C being thin of P st x = B \/ C by Def5;
consider C being thin of P such that
A7: x = B \/ C by A6;
reconsider C1 = C as thin of P2M P by Th23;
x = B \/ C1 by A7;
hence x in COM (Sigma,(P2M P)) by A5, MEASURE3:def 3; :: thesis: verum

end;

hence COM (Sigma,P) = COM (Sigma,(P2M P)) by A1; :: thesis: verum