let x be object ; :: thesis:
let w be Nat; :: thesis:
let m be Integer; :: thesis:
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:
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;

suppose w = 0 ; :: thesis:

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:

end;

suppose ex k being Nat st m = k ; :: thesis:

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:

end;

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

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:

end;

end;