:: deftheorem Def4 defines measure_zero MEASURE1:def 4 :
for X being set
for S being Field_Subset of X
for M being Measure of S
for b₄ being Element of S holds
( b₄ is measure_zero of M iff M . b₄ = 0. );