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