let
n
,
i
be
Nat
;
:: thesis:
(
i
<=
n
implies
i
+
1 is
Nat
of
n
)
assume
i
<=
n
;
:: thesis:
i
+
1 is
Nat
of
n
then
A1
:
i
+
1
<=
n
+
1
by
XREAL_1:7
;
1
<=
i
+
1
by
NAT_1:11
;
hence
i
+
1 is
Nat
of
n
by
A1
,
Def2
;
:: thesis:
verum