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