:: deftheorem Def1 defines C_Measure MEASURE4:def 1 :
for X being set
for b₂ being Function of (bool X),ExtREAL holds
( b₂ is C_Measure of X iff ( b₂ is nonnegative & b₂ is zeroed & ( for A, B being Subset of X st A c= B holds
( b₂ . A <= b₂ . B & ( for F being sequence of (bool X) holds b₂ . (union (rng F)) <= SUM (b₂ * F) ) ) ) ) );