let
n
,
i
be
Nat
;
:: thesis:
(
i
in
the
carrier
of
(
Necklace
n
)
implies
i
<
n
)
assume
i
in
the
carrier
of
(
Necklace
n
)
;
:: thesis:
i
<
n
then
i
in
Segm
n
by
Th19
;
hence
i
<
n
by
NAT_1:44
;
:: thesis:
verum