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
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 r in D1 ; :: thesis: r in D2
then ex k being Element of NAT st r = - k by A2;
hence r in D2 by A3; :: thesis: verum

end;

assume r in D2 ; :: thesis: r in D1
then ex k being Element of NAT st r = - k by A3;
hence r in D1 by A2; :: thesis: verum

end;

hence D1 = D2 by SUBSET_1:8; :: thesis: verum