let x be set ; :: thesis: for l being Element of NAT
for m being Integer st x = m / l holds
x in RAT
let l be Element of NAT ; :: thesis: for m being Integer st x = m / l holds
x in RAT
let m be Integer; :: thesis: ( x = m / l implies x in RAT )
A1: m is Element of INT by INT_1:def 2;
assume A2: x = m / l ; :: thesis: x in RAT
then A3: not x in {[0 ,0 ]} by NUMBERS:def 1, XBOOLE_0:def 5;

per cases ( l = 0 or ex k being Element of NAT st m = k or ( l <> 0 & ( for k being Element of NAT holds m <> k ) ) ) ;

suppose l = 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 Element of NAT st m = k ; :: thesis: x in RAT

then consider k being Element of NAT such that
A4: m = k ;
x = quotient k,l 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: l <> 0 and
A6: for k being Element of NAT holds m <> k ; :: thesis: x in RAT

consider k being Element of NAT such that
A7: m = - k by A1, A6, INT_1:def 1;
A8: k / l = quotient k,l by Lm2;
then k / l in RAT+ ;
then reconsider x9 = k / l as Element of REAL+ by ARYTM_2:1;
A9: 0 in {0 } by TARSKI:def 1;
A10: x = - (k / l) by A2, A7;
m <> 0 by A6;
then A11: x9 <> 0 by A2, A5, A10, XCMPLX_1:50;
x = 09 - x9 by A10, Lm3
.= [0 ,x9] by A11, ARYTM_1:19 ;
then x in [:{0 },RAT+ :] by A8, A9, ZFMISC_1:106;
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;