k - n in NAT by INT_1:5, EC_PF_2:def 1;
hence k - n is natural ; :: thesis: verum