:: deftheorem Def7 defines measure_zero MEASURE1:def 7 :
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Element of S holds
( b₄ is measure_zero of M iff M . b₄ = 0. );