let x be object ; :: thesis: ( x in RAT implies ex m, n being Integer st
( n > 0 & x = m / n ) )
assume A1: x in RAT ; :: thesis: ex m, n being Integer st
( n > 0 & x = m / n )

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: ex m, n being Integer st
( n > 0 & x = m / n )

then x = 0 / 1 ;
hence ex m, n being Integer st
( n > 0 & x = m / n ) ; :: thesis: verum

end;

suppose A2: x <> 0 ; :: thesis: ex m, n being Integer st
( n > 0 & x = m / n )

consider m, n being Integer such that
A3: x = m / n by A1, Def1;

per cases ( n = 0 or n > 0 or n < 0 ) ;

suppose n = 0 ; :: thesis: ex m, n being Integer st
( n > 0 & x = m / n )

hence ex m, n being Integer st
( n > 0 & x = m / n ) by A2, A3, XCMPLX_1:49; :: thesis: verum

end;

suppose A4: n > 0 ; :: thesis: ex m, n being Integer st
( n > 0 & x = m / n )

take m ; :: thesis: ex n being Integer st
( n > 0 & x = m / n )
take n ; :: thesis: ( n > 0 & x = m / n )
thus n > 0 by A4; :: thesis: x = m / n
thus x = m / n by A3; :: thesis: verum

end;

suppose A5: n < 0 ; :: thesis: ex m, n being Integer st
( n > 0 & x = m / n )

take - m ; :: thesis: ex n being Integer st
( n > 0 & x = (- m) / n )
take - n ; :: thesis: ( - n > 0 & x = (- m) / (- n) )
thus - n > 0 by A5, XREAL_1:58; :: thesis: x = (- m) / (- n)
thus x = (- m) / (- n) by A3, XCMPLX_1:191; :: thesis: verum

end;

end;

end;

end;