let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
let P be Probability of Sigma; :: thesis: for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
let Y be Subset of Omega; :: thesis: ( Y is thin of P iff Y is thin of P2M P )

hereby :: thesis: ( Y is thin of P2M P implies Y is thin of P )

assume Y is thin of P ; :: thesis: Y is thin of P2M P
then ex A being set st
( A in Sigma & Y c= A & P . A = 0 ) by Def4;
hence Y is thin of P2M P by MEASURE3:def 2; :: thesis: verum

end;

assume Y is thin of P2M P ; :: thesis: Y is thin of P
then ex B being set st
( B in Sigma & Y c= B & (P2M P) . B = 0. ) by MEASURE3:def 2;
hence Y is thin of P by Def4; :: thesis: verum