let p be rational number ; :: thesis: ( p >= 0 implies ex m, n being Nat st
( n <> 0 & p = m / n ) )
consider m being Integer, k being Element of NAT such that
A1: ( k <> 0 & p = m / k ) by RAT_1:24;
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:143;
then reconsider m = m as Element of NAT by INT_1:16;
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