:: deftheorem Def8 defines pre-Measure MEASURE9:def 7 :
for X being set
for P being with_empty_element Subset-Family of X
for b₃ being zeroed nonnegative Function of P,ExtREAL holds
( b₃ is pre-Measure of P iff ( ( for F being disjoint_valued FinSequence of P st Union F in P holds
b₃ . (Union F) = Sum (b₃ * F) ) & ( for K being disjoint_valued Function of NAT,P st Union K in P holds
b₃ . (Union K) <= SUM (b₃ * K) ) ) );