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 object ; :: 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
reconsider xx = x as set by TARSKI:1;
(P_COM2M_COM A) \ xx is thin of P2M P by A2, MEASURE3:def 4;
then A3: A \ xx is thin of P by Th23;
( x in Sigma & xx c= P_COM2M_COM A ) by A2, MEASURE3:def 4;
hence x in ProbPart A by A3, Def7; :: thesis: verum

end;

ProbPart A c= MeasPart (P_COM2M_COM A)

proof

let x be object ; :: 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)
reconsider xx = x as set by TARSKI:1;
A \ xx is thin of P by A4, Def7;
then A5: (P_COM2M_COM A) \ xx is thin of P2M P by Th23;
( x in Sigma & xx c= A ) by A4, Def7;
hence x in MeasPart (P_COM2M_COM A) by A5, MEASURE3:def 4; :: thesis: verum

end;

hence ProbPart A = MeasPart (P_COM2M_COM A) by A1; :: thesis: verum