let p be Rational; :: thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k )
consider m, n being Integer such that
A1: ( n <> 0 & p = m / n ) by Th3;

per cases ( 0 < n or n < 0 ) by A1;

suppose 0 < n ; :: thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k )

then n is Element of NAT by INT_1:16;
hence ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k ) by A1; :: thesis: verum

end;

suppose n < 0 ; :: thesis: ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k )

then 0 <= - n ;
then A2: - n is Element of NAT by INT_1:16;
A3: p = - ((- m) / n) by A1
.= (- m) / (- n) by XCMPLX_1:189 ;
- n <> 0 by A1;
hence ex m being Integer ex k being Element of NAT st
( k <> 0 & p = m / k ) by A2, A3; :: thesis: verum

end;

end;