let D1, D2 be Subset of REAL ; :: thesis: ( ( for r being Real holds
( r in D1 iff ex k being Element of NAT st r = - k ) ) & ( for r being Real holds
( r in D2 iff ex k being Element of NAT st r = - k ) ) implies D1 = D2 )
assume that
A2: for r being Real holds
( r in D1 iff ex k being Element of NAT st r = - k ) and
A3: for r being Real holds
( r in D2 iff ex k being Element of NAT st r = - k ) ; :: thesis: D1 = D2
A4: for r being Real holds
( r in D1 iff r in D2 )

proof

let r be Real; :: thesis: ( r in D1 iff r in D2 )
thus ( r in D1 implies r in D2 ) :: thesis: ( r in D2 implies r in D1 )

proof

assume A5: r in D1 ; :: thesis: r in D2
A6: ex k being Element of NAT st r = - k by A2, A5;
thus r in D2 by A3, A6; :: thesis: verum

end;

assume A7: r in D2 ; :: thesis: r in D1
A8: ex k being Element of NAT st r = - k by A3, A7;
thus r in D1 by A2, A8; :: thesis: verum

end;

thus D1 = D2 by A4, SUBSET_1:8; :: thesis: verum