n

2
>=
2

2
by
EC_PF_2:def 1
,
XREAL_1:9
;
then
n

2
in
NAT
by
INT_1:3
;
hence
n

2 is
natural
;
:: thesis:
verum