IC in dom p by Th6;
hence IncIC (p,k) is Reloc (q,k) -halted by Th12; :: thesis: verum