:: deftheorem Def9 defines J-Meas MEASUR12:def 9 :
for b₁ being Measure of (Field_generated_by Family_of_Intervals) holds
( b₁ = J-Meas iff for A being set st A in Field_generated_by Family_of_Intervals holds
for F being disjoint_valued FinSequence of Family_of_Intervals st A = Union F holds
b₁ . A = Sum (pre-Meas * F) );