let
n
be
Nat
;
:: thesis:
(
n
>=
3 implies
n
+`
n
in
exp
(2,
n
) )
assume
AS
:
n
>=
3 ;
:: thesis:
n
+`
n
in
exp
(2,
n
)
n
+`
n
=
n
+
n
by
th0a
;
then
n
+`
n
<
2
|^
n
by
AS
,
th0n
;
then
n
+`
n
in
2
|^
n
by
th0k
;
hence
n
+`
n
in
exp
(2,
n
)
by
th0e
;
:: thesis:
verum