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