Solution (source code)

= Solution

Because the <vertex set> is finite, at least one vertex occurs infinitely often, so $\operatorname{Inf}(\rho)$ is nonempty. Let $u,v$ belong to this set. After any chosen visit to $u$, a later visit to $v$ exists; the intervening edges give a directed walk from $u$ to $v$. After that visit to $v$, a later visit to $u$ also exists, giving a walk in the other direction. Removing repeated portions gives <directed paths> if desired.

Thus every pair in $\operatorname{Inf}(\rho)$ is mutually reachable and belongs to the same <strongly connected component>. This proves the claimed inclusion, which need not be equality: an infinite walk can repeatedly follow one cycle while omitting other vertices in its component. This is the recurrence-set part of the <infinite walk criterion in a finite directed graph>.