defpred S_{1}[ 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_{1}[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

consider D being set such that

A1: for x being object holds

( x in D iff ( x in ExtREAL & S

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