For an mso relabelling with formulas $\Phi$, the language over $A \times \Phi$ of the strings $(a_1, \varphi_1) \cdots (a_n, \varphi_n)$ such that for every $i$ the formula $\varphi_i$ is true at position $i$ of $a_1 \cdots a_n$ is regular (Claim C.4.6 of Transducers). For each formula, the strings with one marked position at which the formula holds form a regular language by Lemma C.4.2, and the claim's language is the intersection, over the formulas, of the complements of the projections of the strings that violate it.