:: deftheorem defines complete MEASURE3:def 1 :
for X being set
for Sigma being SigmaField of X
for M being sigma_Measure of Sigma holds
( M is complete iff for A being Subset of X
for B being set st B in Sigma & A c= B & M . B = 0. holds
A in Sigma );