let k be natural number ; :: 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:11;
hence k - 2 is Element of NAT by INT_1:16; :: thesis: verum