[morelisp]

> By which process do you do that?

It's not a constructive proof, you don't need to give a process.

[kotlin2]

That's true. The part that "feels" weird is that there is no algorithm that could perform the separation into halting / non-halting subsets. Choosing elements from a set based on uncomputable properties almost feels like an extension of the axiom of choice.