for l being Instruction-Location of SCMPDS holds NIC (saveIC a,k1),l = {(Next l)} by Th11;
hence JUMP (saveIC a,k1) is empty by Th8; :: thesis: verum