for
l
being
Element
of
NAT
holds
NIC
(
(
SubFrom
(
a
,
b
)
)
,
l
)
=
{
(
l
+
1
)
}
by
AMISTD_1:12
;
hence
JUMP
(
SubFrom
(
a
,
b
)
)
is
empty
by
Lm1
;
:: thesis:
verum