Take the quasi-wideness margins $N, s$ of the class at radius $r$ from the endorsed $Lax12.NowhereDenseUQW.uniformlyQuasiWide_of_nowhereDense$ and put $ℓ := N (2·s + 2)$ and $m := ℓ · (r + 1)$. Splitter's strategy isolates, in each round, Connector's new vertex $v$ together with the still-active vertices of a chosen walk of length at most $r$ from every earlier Connector vertex to $v$, taken in the arena that earlier round was played in — one vertex plus one path of at most $r + 1$ vertices per round played, which is the bound $m$. A play in which every Connector move still had an incident edge is recorded by $Reached$; moves on isolated vertices end the play at once, since the ball around such a vertex is the vertex alone.

The whole content is that no play lasts $ℓ$ rounds. Connector's vertices are then $ℓ$ distinct vertices, so quasi-wideness returns a separator $S$ of at most $s$ vertices and a distance-$r$ independent set $B$ of at least $2·s + 2$ of them. Pairing the rounds that selected a vertex of $B$ off chronologically gives $s + 1$ pairs, and for each the strategy's maintained walk between the pair's two vertices, in the older round's arena. Two ingredients replace the notes' "removed vertices are gone". Isolation is permanent: arenas only lose edges, so a vertex the strategy isolated in some round has no incident edge in any later arena. Distinct pairs' walks are disjoint: a vertex of an older pair's walk was isolated when that pair's newer round was played, while every vertex of a newer pair's walk carries an edge in an arena from strictly after that round. So the $s + 1$ walks are pairwise disjoint and one of them avoids $S$; rebuilding it inside $deleteVerts G S$ gives a walk of length at most $r$ between two distinct members of $B$, contradicting the independence.

The round bound is $N (2·s + 2)$, not the notes' $N (2·s + 1)$: their own proof needs $s + 1$ pairwise disjoint paths so that one avoids the separator, which is $2·s + 2$ selected rounds. See the module docstring.