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 set ; :: 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 4;
consider C being thin of P2M P such that
A4: x = B \/ C by A3;
reconsider C1 = C as thin of P by Th24;
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 set ; :: 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 Th24;
x = B \/ C1 by A7;
hence x in COM Sigma,(P2M P) by A5, MEASURE3:def 4; :: thesis: verum

end;

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