{
k
where
k
is
Nat
:
k
>
1 } is
infinite
by
PRE_CIRC:23
;
hence
not
JUMP
(
return
a
)
is
finite
by
Th17
;
:: thesis:
verum