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