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

per cases ( x in RAT+ or x in [:{0 },RAT+ :] ) by A1, NUMBERS:def 3, XBOOLE_0:def 3;

suppose x in RAT+ ; :: thesis: ex m, n being Integer st x = m / n

then reconsider x = x as Element of RAT+ ;
take numerator x ; :: thesis: ex n being Integer st x = (numerator x) / n
take denominator x ; :: thesis: x = (numerator x) / (denominator x)
quotient (numerator x),(denominator x) = x by ARYTM_3:45;
hence x = (numerator x) / (denominator x) by Lm2; :: thesis: verum

end;

suppose x in [:{0 },RAT+ :] ; :: thesis: ex m, n being Integer st x = m / n

then consider x1, x2 being set such that
A2: x1 in {0 } and
A3: x2 in RAT+ and
A4: x = [x1,x2] by ZFMISC_1:103;
reconsider x2 = x2 as Element of RAT+ by A3;
reconsider x' = x2 as Element of REAL+ by A3, ARYTM_2:1;
take m = - (numerator x2); :: thesis: ex n being Integer st x = m / n
take n = denominator x2; :: thesis: x = m / n
A5: x2 = quotient (numerator x2),(denominator x2) by ARYTM_3:45
.= (numerator x2) / n by Lm2 ;
A6: x1 = 0 by A2, TARSKI:def 1;
A7: x = [0 ,x'] by A2, A4, TARSKI:def 1;
not x in {[0 ,0 ]} by A1, NUMBERS:def 3, XBOOLE_0:def 5;
then x2 <> 0 by A7, TARSKI:def 1;
hence x = 0' - x' by A4, A6, ARYTM_1:19
.= - ((numerator x2) / n) by A5, Lm3
.= m / n ;
:: thesis: verum

end;

end;