let r be Element of F_Rat; :: thesis: ex K being Integer st

( K <> 0 & K * r in INT )

consider m, n being Integer such that

P1: ( n <> 0 & r = m / n ) by RAT_1:1;

take n ; :: thesis: ( n <> 0 & n * r in INT )

thus n <> 0 by P1; :: thesis: n * r in INT

n * r = m by P1, XCMPLX_1:87;

hence n * r in INT by INT_1:def 2; :: thesis: verum

( K <> 0 & K * r in INT )

consider m, n being Integer such that

P1: ( n <> 0 & r = m / n ) by RAT_1:1;

take n ; :: thesis: ( n <> 0 & n * r in INT )

thus n <> 0 by P1; :: thesis: n * r in INT

n * r = m by P1, XCMPLX_1:87;

hence n * r in INT by INT_1:def 2; :: thesis: verum