let x be object ; :: thesis: for w being Nat
for m being Integer st x = m / w holds
x in RAT
let w be Nat; :: thesis: for m being Integer st x = m / w holds
x in RAT
let m be Integer; :: thesis: ( x = m / w implies x in RAT )
reconsider Z9 = 0 as Element of REAL+ by ARYTM_2:2;
A1: m is Element of INT by INT_1:def 2;
assume A2: x = m / w ; :: thesis: x in RAT
then x in REAL by XREAL_0:def 1;
then A3: not x in {[0,0]} by NUMBERS:def 1, XBOOLE_0:def 5;
reconsider w = w as Element of NAT by ORDINAL1:def 12;

per cases ( w = 0 or ex k being Nat st m = k or ( w <> 0 & ( for k being Nat holds m <> k ) ) ) ;

suppose w = 0 ; :: thesis: x in RAT

then x = m * (0 ") by A2
.= 0 ;
then x in RAT+ \/ [:{0},RAT+:] by Lm1, XBOOLE_0:def 3;
hence x in RAT by A3, NUMBERS:def 3, XBOOLE_0:def 5; :: thesis: verum

end;

suppose ex k being Nat st m = k ; :: thesis: x in RAT

then consider k being Nat such that
A4: m = k ;
x = quotient (k,w) by A2, A4, Lm2;
then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 3;
hence x in RAT by A3, NUMBERS:def 3, XBOOLE_0:def 5; :: thesis: verum

end;

suppose that A5: w <> 0 and
A6: for k being Nat holds m <> k ; :: thesis: x in RAT

consider k being Nat such that
A7: m = - k by A1, A6, INT_1:def 1;
A8: k / w = quotient (k,w) by Lm2;
then k / w in RAT+ ;
then reconsider x9 = k / w as Element of REAL+ by ARYTM_2:1;
A9: 0 in {0} by TARSKI:def 1;
A10: x = - (k / w) by A2, A7;
m <> 0 by A6;
then A11: x9 <> 0 by A2, A5, A10, XCMPLX_1:50;
x = Z9 - x9 by A10, Lm3
.= [0,x9] by A11, ARYTM_1:19 ;
then x in [:{0},RAT+:] by A8, A9, ZFMISC_1:87;
then x in RAT+ \/ [:{0},RAT+:] by XBOOLE_0:def 3;
hence x in RAT by A3, NUMBERS:def 3, XBOOLE_0:def 5; :: thesis: verum

end;

end;