:: deftheorem Def5 defines sigma-additive MEASURE1:def 5 :
for X being set
for IT being Subset-Family of X holds
( IT is sigma-additive iff for M being N_Sub_set_fam of X st M c= IT holds
union M in IT );