i
<
2
to_power
n
by
A1
;
then
(
2
to_power
n
)

i
>
i

i
by
XREAL_1:9
;
then
(
2
to_power
n
)

i
is
Element
of
NAT
by
INT_1:3
;
hence
(
2
to_power
n
)

i
is
Nat
;
:: thesis:
verum