let
x
be
object
;
:: thesis:
(
x
is
integer
implies
x
is
rational
)
assume
x
is
integer
;
:: thesis:
x
is
rational
then
reconsider
x
=
x
as
Integer
;
x
=
x
/
1 ;
hence
x
is
rational
by
Th3
;
:: thesis:
verum