:: deftheorem defines is_complete PROB_4:def 3 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma );