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

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

assume A5: q in D1 ; :: thesis:
reconsider q = q as Rational ;
ex i being Integer st q = i / n by A3, A5;
hence q in D2 by A4; :: thesis:

end;

assume A6: q in D2 ; :: thesis:
reconsider q = q as Rational ;
ex i being Integer st q = i / n by A4, A6;
hence q in D1 by A3; :: thesis:

end;