:: deftheorem Def3 defines additive MEASURE1:def 3 :
for X being set
for S being non empty Subset-Family of X
for F being Function of S,ExtREAL holds
( F is additive iff for A, B being Element of S st A misses B & A \/ B in S holds
F . (A \/ B) = (F . A) + (F . B) );