for l being Instruction-Location of SCM holds NIC (Divide a,b),l = {(Next )} by Th45;
hence JUMP (Divide a,b) is empty by Lm5; :: thesis: verum