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