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 A2: x in [:{0 },RAT+ :] ; :: thesis: ex m, n being Integer st x = m / n

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

end;

end;