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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in MeasPart (P_COM2M_COM A) or x in ProbPart A )
assume A2: x in MeasPart (P_COM2M_COM A) ; :: thesis: x in ProbPart A
(P_COM2M_COM A) \ x is thin of P2M P by A2, MEASURE3:def 5;
then A3: A \ x is thin of P by Th24;
( x in Sigma & x c= P_COM2M_COM A ) by A2, MEASURE3:def 5;
hence x in ProbPart A by A3, Def7; :: thesis: verum

end;

ProbPart A c= MeasPart (P_COM2M_COM A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ProbPart A or x in MeasPart (P_COM2M_COM A) )
assume A4: x in ProbPart A ; :: thesis: x in MeasPart (P_COM2M_COM A)
A \ x is thin of P by A4, Def7;
then A5: (P_COM2M_COM A) \ x is thin of P2M P by Th24;
( x in Sigma & x c= A ) by A4, Def7;
hence x in MeasPart (P_COM2M_COM A) by A5, MEASURE3:def 5; :: thesis: verum

end;

hence ProbPart A = MeasPart (P_COM2M_COM A) by A1, XBOOLE_0:def 10; :: thesis: verum