defpred S₁[ object ] means ex CA being Covering of A,F st $1 = SUM (vol (M,CA));
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 CA being Covering of A,F st x = SUM (vol (M,CA)) )
thus for x being R_eal holds
( x in D iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) by A1; :: thesis: verum