let
x
be
object
;
:: thesis:
for
m
,
n
being
Integer
st
x
=
m
/
n
holds
x
in
RAT
let
m
,
n
be
Integer
;
:: thesis:
(
x
=
m
/
n
implies
x
in
RAT
)
assume
A1
:
x
=
m
/
n
;
:: thesis:
x
in
RAT
n
is
Element
of
INT
by
INT_1:def 2
;
then
consider
k
being
Nat
such that
A2
: (
n
=
k
or
n
=

k
)
by
INT_1:def 1
;
per
cases
(
n
=
k
or
n
=

k
)
by
A2
;
suppose
n
=
k
;
:: thesis:
x
in
RAT
hence
x
in
RAT
by
A1
,
Lm5
;
:: thesis:
verum
end;
suppose
n
=

k
;
:: thesis:
x
in
RAT
then
x
=
(

m
)
/
k
by
A1
,
XCMPLX_1:192
;
hence
x
in
RAT
by
Lm5
;
:: thesis:
verum
end;
end;