let
n
be
Nat
;
:: thesis:
1
in
Seg
(
n
+
1
)
0
<=
n
by
NAT_1:2
;
then
0
+
1
<=
n
+
1
by
XREAL_1:7
;
hence
1
in
Seg
(
n
+
1
)
by
FINSEQ_1:1
;
:: thesis:
verum