for
f
being
Nat
holds
NIC
(
I
,
f
)
=
{
f
}
by
AMISTD_1:2
,
AMISTD_1:17
;
hence
JUMP
I
is
empty
by
AMISTD_1:1
;
:: thesis:
verum