for l being Element of NAT holds NIC ((saveIC (a,k1)),l) = {(l + 1)} by Th5;
hence JUMP (saveIC (a,k1)) is empty by Th2; :: thesis: verum