let x be object ; :: thesis: for m, n being Integer st x = m / n holds
x in RAT
let m, n be Integer; :: thesis: ( x = m / n implies x in RAT )
assume A1: x = m / n ; :: thesis: x in RAT
n is Element of INT by INT_1:def 2;
then consider k being Nat such that
A2: ( n = k or n = - k ) by INT_1:def 1;

per cases ( n = k or n = - k ) by A2;

suppose n = k ; :: thesis: x in RAT

hence x in RAT by A1, Lm5; :: thesis: verum

end;

suppose n = - k ; :: thesis: x in RAT

then x = (- m) / k by A1, XCMPLX_1:192;
hence x in RAT by Lm5; :: thesis: verum

end;

end;