Borel separation of disjoint analytic sets

If $A=\mathrm{\varnothing }$ take $C=\mathrm{\varnothing }$; if $B=\mathrm{\varnothing }$ take $C=X$. Otherwise by F1, licensed by A1, fix continuous $f,g:\mathcal{N}\to X$ with images $A,B$. For finite words $s,t$ write $A_s=f[N_s]$ and $B_t=g[N_t]$.

Suppose every child pair $A_{s^{⌢}n},B_{t^{⌢}m}$ has a Borel separator. A1 selects separators $C_{nm}$ from the nonempty subsets of $\mathcal{P}(X)$ satisfying this property. Then $C={\bigcup }_n{\bigcap }_m{C}_{nm}$ is Borel by F2 and De Morgan's identity. Every point of $A_s$ lies in a child $A_{s^{⌢}n}$ and hence in every $C_{nm}$ for that n, so in $C$. Every point of $B_t$ lies in some $B_{t^{⌢}m}$ and hence outside $C_{nm}$ for each n, so outside $C$. Thus $C$ separates the parent pair.

If $A,B$ were inseparable, step 1.2 implies that each inseparable pair has an inseparable child pair. Recursively take the least such pair of child indices in a fixed enumeration of ${\mathbb{N}}^2$. This produces words $s_n,t_n$ of length n whose image pairs remain inseparable. Let $a={\bigcup }_n{s}_n$ and $b={\bigcup }_n{t}_n$. Disjointness gives $f(a)\mathrm{\ne }g(b)$. Choose disjoint metric open neighbourhoods $U,V$ of these points. Continuity gives a common n with $f[N_{s_n}]\subseteq U$ and $g[N_{t_n}]\subseteq V$. Then Borel $U$ separates this pair, a contradiction. Therefore a Borel separator exists. The two branches $a,b$ have been constructed independently; no equality between them is assumed. QED.