let
k
be
Nat
;
:: thesis:
(
k
>
1 implies
k

2 is
Element
of
NAT
)
assume
k
>
1 ;
:: thesis:
k

2 is
Element
of
NAT
then
k
>=
1
+
1
by
NAT_1:13
;
then
k

2
>=
2

2
by
XREAL_1:9
;
hence
k

2 is
Element
of
NAT
by
INT_1:3
;
:: thesis:
verum