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