defpred S_{1}[ set ] means ex CA being Covering of A,F st $1 = SUM (vol (M,CA));

let D1, D2 be Subset of ExtREAL; :: thesis: ( ( for x being R_eal holds

( x in D1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds

( x in D2 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) implies D1 = D2 )

assume that

A2: for x being R_eal holds

( x in D1 iff S_{1}[x] )
and

A3: for x being R_eal holds

( x in D2 iff S_{1}[x] )
; :: thesis: D1 = D2

thus D1 = D2 from SUBSET_1:sch 2(A2, A3); :: thesis: verum

let D1, D2 be Subset of ExtREAL; :: thesis: ( ( for x being R_eal holds

( x in D1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds

( x in D2 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) implies D1 = D2 )

assume that

A2: for x being R_eal holds

( x in D1 iff S

A3: for x being R_eal holds

( x in D2 iff S

thus D1 = D2 from SUBSET_1:sch 2(A2, A3); :: thesis: verum