let p be Rational; :: thesis: ex m being Integer ex k being Nat st
( k > 0 & p = m / k )
consider m, n being Integer such that
A1: n > 0 and
A2: p = m / n by Th2;

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

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

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

end;

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

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

end;

end;