The hypothesis is $Lax12.NowhereDense$ verbatim, and the proof to come derives the strategy from Lax12's $uniformlyQuasiWide_of_nowhereDense$, following the notes' path-maintenance strategy: Splitter maintains BFS paths to the connector vertices of earlier rounds and isolates the still-active vertices of those paths, with $ℓ = N_r(2·s_r + 2)$ and $m = ℓ · (r + 1)$ for the quasi-wideness margins $N_r, s_r$. Two remarks recorded for the discharge. First, the notes state $ℓ = N_r(2·s_r + 1)$, but their proof extracts $s_r + 1$ pairwise disjoint paths so that one avoids the deleted separator, which needs the $+ 2$ form; the formalization takes the $+ 2$ form and fixes the slip silently. Second, the isolation variant needs no new argument over the notes' deletion variant: arenas only lose edges, so a vertex isolated in some round has no incident edge in any later arena — the paths the strategy cuts stay cut, and the distance-independent set the contradiction extracts is independent in exactly Lax12's $deleteVerts$ sense, which is the conclusion shape of the endorsed quasi-wideness theorem.

The statement quantifies the strategy away: it asserts winning positions, not a strategy function. The explicit strategy — the object the model-checking program executes — is constructed proofs-side with this axiom's discharge and consumed there by the program-correctness proofs; surfacing it would freeze implementation detail into the concept.