theorem Th3: :: RAT_1:3

for m, n being Integer holds m / n is rational by Def1;