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