let x be object ; :: 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 by ;
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 = () / n
take denominator x ; :: thesis: x = () / ()
quotient ((),()) = x by ARYTM_3:39;
hence x = () / () by Lm2; :: thesis: verum
end;
suppose A2: x in ; :: thesis: ex m, n being Integer st x = m / n
A3: not x in by ;
consider x1, x2 being object such that
A4: x1 in and
A5: x2 in RAT+ and
A6: x = [x1,x2] by ;
reconsider x2 = x2 as Element of RAT+ by A5;
reconsider x9 = x2 as Element of REAL+ by ARYTM_2:1;
x = [0,x9] by ;
then A7: x2 <> 0 by ;
take m = - (); :: thesis: ex n being Integer st x = m / n
take n = denominator x2; :: thesis: x = m / n
reconsider Z9 = 0 as Element of REAL+ by ARYTM_2:2;
A8: x2 = quotient ((),()) by ARYTM_3:39
.= () / n by Lm2 ;
x1 = 0 by ;
hence x = Z9 - x9 by
.= - (() / n) by
.= m / n ;
:: thesis: verum
end;
end;