:: deftheorem Def7 defines Svc2 MEASUR12:def 7 :
for A being Subset of REAL
for b₂ being Subset of ExtREAL holds
( b₂ = Svc2 A iff for x being R_eal holds
( x in b₂ iff ex F being Open_Interval_Covering of A st x = vol F ) );