let p be Rational; :: thesis: ( p >= 0 implies ex m, n being Nat st
( n <> 0 & p = m / n ) )
consider m being Integer, k being Nat such that
A1: ( k <> 0 & p = m / k ) by RAT_1:8;
assume p >= 0 ; :: thesis: ex m, n being Nat st
( n <> 0 & p = m / n )
then ( ( k > 0 & m >= 0 ) or ( k < 0 & m <= 0 ) ) by A1, XREAL_1:141;
then reconsider m = m as Element of NAT by INT_1:3;
take m ; :: thesis: ex n being Nat st
( n <> 0 & p = m / n )
take k ; :: thesis: ( k <> 0 & p = m / k )
thus ( k <> 0 & p = m / k ) by A1; :: thesis: verum