Strong Zilber–Pink conjecture I for atypical subvarieties

Let $S$ be a Shimura variety and let $V$ be an irreducible subvariety of $S$. An irreducible subvariety $W$ of $V$ is called atypical if it is an irreducible component of $V\cap Z$ for a special subvariety $Z$ of $S$ and satisfies

$$\dim W>\dim V+\dim Z-\dim S.$$

Write $\operatorname{Atyp}(V)$ for the union of the atypical subvarieties of $V$. Strong Zilber–Pink I. Then $\operatorname{Atyp}(V)$ is equal to a finite union of atypical subvarieties of $V$. This is presented as an ostensibly stronger formulation of Zilber–Pink and is known to be equivalent to it for a fixed Shimura variety under the cited results; the general conjecture remains open.