let D1, D2 be Subset of RAT ; :: thesis: ( ( for q being Rational holds
( q in D1 iff ex i being Integer st q = i / n ) ) & ( for q being Rational holds
( q in D2 iff ex i being Integer st q = i / n ) ) implies D1 = D2 )
assume that
A4: for q being Rational holds
( q in D1 iff ex i being Integer st q = i / n ) and
A5: for q being Rational holds
( q in D2 iff ex i being Integer st q = i / n ) ; :: thesis: D1 = D2
A6: for q being Element of RAT holds
( q in D1 iff q in D2 )

proof

let q be Element of RAT ; :: thesis: ( q in D1 iff q in D2 )
thus ( q in D1 implies q in D2 ) :: thesis: ( q in D2 implies q in D1 )

proof

assume A7: q in D1 ; :: thesis: q in D2
reconsider q = q as Rational ;
A8: ex i being Integer st q = i / n by A4, A7;
thus q in D2 by A5, A8; :: thesis: verum

end;

assume A9: q in D2 ; :: thesis: q in D1
reconsider q = q as Rational ;
A10: ex i being Integer st q = i / n by A5, A9;
thus q in D1 by A4, A10; :: thesis: verum

end;

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