for l being Element of NAT holds NIC (a := b),l = {(succ l)} by Th54;
hence JUMP (a := b) is empty by Lm5; :: thesis: verum