let
n
,
i
be
Nat
;
:: thesis:
(
i
is
Nat
of
n
iff
i
in
Seg
(
n
+
1
)
)
(
i
is
Nat
of
n
iff ( 1
<=
i
&
i
<=
n
+
1 ) )
by
Def2
;
hence
(
i
is
Nat
of
n
iff
i
in
Seg
(
n
+
1
)
)
by
FINSEQ_1:1
;
:: thesis:
verum