Independent loxodromics have disjoint pole neighbourhoods

List the poles as $p_1,p_2,p_3,p_4$, placing the positive and negative poles of the first isometry before those of the second. By F1 each pair is distinct and the two pairs are disjoint, so all four points are distinct.

For each of the six pairs $i<j$, F2 supplies disjoint open sets $V_{ij}$ containing $p_i$ and $W_{ij}$ containing $p_j$. Fix these six pairs of sets successively; this is finite existential instantiation, not an invocation of AC. Define $O_i={\bigcap }_{j>i}{V}_{ij}\cap {\bigcap }_{j<i}{W}_{ji}$. An intersection with no indices denotes the whole boundary. Each $O_i$ is open as a finite intersection of open sets and contains $p_i$.

If $i<j$, then $O_i\subseteq V_{ij}$ and $O_j\subseteq W_{ij}$, hence $O_i\cap O_j=\mathrm{\varnothing }$. Thus these are the four required open neighbourhoods. Repeated poles, an empty boundary or a singleton boundary are excluded by step 1.1; empty sub-intersections in step 2.1 cause no restriction. This construction assumes the two independent isometries and asserts no existence of such a pair.