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

hereby :: thesis: ( P2M P is_complete Sigma implies P is_complete Sigma )

assume P is_complete Sigma ; :: thesis: P2M P is_complete Sigma
then for A being Subset of Omega
for B being set st B in Sigma & A c= B & (P2M P) . B = 0. holds
A in Sigma by Def3;
hence P2M P is_complete Sigma by MEASURE3:def 1; :: thesis: verum

end;

assume P2M P is_complete Sigma ; :: thesis: P is_complete Sigma
then for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma by MEASURE3:def 1;
hence P is_complete Sigma by Def3; :: thesis: verum