consider D being set such that
A1: for x being object holds
( x in D iff ( x in ExtREAL & S₁[x] ) ) from XBOOLE_0:sch 1();
for z being object st z in D holds
z in ExtREAL by A1;
then reconsider D = D as Subset of ExtREAL by TARSKI:def 3;
take D ; :: thesis: for x being R_eal holds
( x in D iff ex F being Interval_Covering of A st x = vol F )
thus for x being R_eal holds
( x in D iff ex F being Interval_Covering of A st x = vol F ) by A1; :: thesis: verum