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