let D1, D2 be Subset of ExtREAL; :: thesis: ( ( for x being R_eal holds
( x in D1 iff ex F being Open_Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in D2 iff ex F being Open_Interval_Covering of A st x = vol F ) ) 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