:: deftheorem Def1 defines N_Measure_fam MEASURE2:def 1 :
for X being set
for S being SigmaField of X
for b₃ being N_Sub_set_fam of X holds
( b₃ is N_Measure_fam of S iff b₃ c= S );