defpred S₁[ 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₁[x] ) and
A3: for x being R_eal holds
( x in D2 iff S₁[x] ) ; :: thesis: D1 = D2
thus D1 = D2 from SUBSET_1:sch 2(A2, A3); :: thesis: verum