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