let D1, D2 be Subset of ExtREAL ; :: thesis: ( ( for x being R_eal holds
( x in D1 iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in D2 iff ex F being Interval_Covering of A st x = vol F ) ) implies D1 = D2 )
assume that
Z1: for x being R_eal holds
( x in D1 iff S₁[x] ) and
Z2: for x being R_eal holds
( x in D2 iff S₁[x] ) ; :: thesis: D1 = D2
thus D1 = D2 from SUBSET_1:sch 2(Z1, Z2); :: thesis: verum