let
n
be
Nat
;
:: thesis:
1 is
Nat
of
n
1
in
Seg
(
n
+
1
)
by
Th20
;
hence
1 is
Nat
of
n
by
Th7
;
:: thesis:
verum