:: deftheorem Def7 defines Svc MEASURE8:def 7 :
for X being set
for F being Field_Subset of X
for M being Measure of F
for A being Subset of X
for b₅ being Subset of ExtREAL holds
( b₅ = Svc (M,A) iff for x being R_eal holds
( x in b₅ iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) );