for l being Element of NAT holds NIC ((saveIC (a,k1)),l) = {(succ l)} by Th11;
hence JUMP (saveIC (a,k1)) is empty by Th8; :: thesis: verum