:: deftheorem Def8 defines Svc MEASURE7:def 8 :
for A being Subset of REAL
for b₂ being Subset of ExtREAL holds
( b₂ = Svc A iff for x being R_eal holds
( x in b₂ iff ex F being Interval_Covering of A st x = vol F ) );