for f being Element of NAT holds NIC (I,f) = {f} by AMISTD_1:15, AMISTD_1:56;
hence JUMP I is empty by AMISTD_1:14; :: thesis: verum