:: deftheorem Def8 defines C_Meas MEASURE8:def 8 :
for X being set
for F being Field_Subset of X
for M being Measure of F
for b₄ being Function of (bool X),ExtREAL holds
( b₄ = C_Meas M iff for A being Subset of X holds b₄ . A = inf (Svc (M,A)) );