:: deftheorem defines additive MEASURE1:def 8 :
for X being set
for S being Field_Subset 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 holds
F . (A \/ B) = (F . A) + (F . B) );