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;

( 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;

end;

suppose
0 < n
; :: thesis: ex m being Integer ex k being Nat st

( k <> 0 & p = m / k )

( 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;hence ex m being Integer ex k being Nat st

( k <> 0 & p = m / k ) by A1, A2; :: thesis: verum

suppose A3:
n < 0
; :: thesis: ex m being Integer ex k being Nat st

( k <> 0 & p = m / k )

( 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;.= (- 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