A C² leaf meets a local box transversal in at most countably many points

Fix the second-countable $C^2$ foliated manifold, the leaf $L$, the foliation box $Q$ and the vertical transverse interval $\tau$, and if the leaf dimension is zero, every plaque and hence every leaf is a singleton, so the intersection has at most one point and the conclusion is immediate. Otherwise fix one plaque $P_0$ of $L$ inside the recorded atlas; a vertical interval meets each plaque of $Q$ in at most one point, because the transverse coordinate is constant on a plaque while $\tau$ varies only in the transverse direction.

By [F1] the second-countable manifold has a countable cover by foliation boxes; selecting one foliation chart for each member of that countable subcover uses the stated countable choice, and adjoin the specified box $Q$ and the box of the initial plaque $P_0$ to that countable atlas (a finite addition), and record this enlarged countable atlas as fixed data for the rest of the argument.

Say a plaque is reached when it can be joined to $P_0$ by a finite chain of plaques of the recorded atlas in which consecutive plaques intersect; every plaque of $L$ is reached by definition of the plaque-chain relation, and it suffices to count the reached plaques contained in $Q$.

Let $P$ be a reached plaque in a box $U$ and let $V$ be a next box of the recorded atlas; in plaque coordinates the trace of $P$ inside $V$ is an open subset of the plaque coordinate space ${\mathbb{R}}^{\dim L}$, whose connected components are open and polygonally connected by [F2]; each nonempty component lies in a single plaque of $V$, because the plaques of $V$ partition the open set $L\cap V$ into pairwise disjoint open subsets of the leaf, so a connected subset of $L\cap V$ cannot meet two of them; code each nonempty component by the least rational-box basis index contained in it, so distinct components, being disjoint, receive distinct codes, and given the current plaque $P$ and the next box $V$ the component code therefore determines at most one successor plaque.

Encode each finite chain of successor data by the natural-number coding of finite sequences from [F3], and assign to each reached plaque in $Q$ the least code of a finite chain reaching it; this is a well-defined injection of the reached plaques of $Q$ into $\mathbb{N}$ and does not select a chain at each plaque.

The reached plaques of $L$ inside $Q$ are therefore at most countable, and by step 1.1 each of them meets $\tau$ in at most one point, so ${\tau }^{-1}(L)$ injects into a countable set and is at most countable; a countable box atlas already supplied as data removes the only countable choice of step 1.2, and dense or nonembedded leaves are allowed since only plaque chains were used.