A finitely cornered regular plane curve separates without choice

Orient $c(S^1)$ by the parameter; since $S^1$ is a closed bounded subset of the plane it is compact by [F7], any open cover of $c(S^1)$ pulls back along the continuous bijection $c$ to an open cover of $S^1$, so $c(S^1)$ is compact, and it is closed in the plane.

At a smooth edge point choose linear coordinates with the tangent horizontal; the first coordinate has nonzero derivative along the edge, so after shrinking it has one sign, [F8] makes it strictly monotone, [F9] shows its image is an interval, and its inverse is $C^1$ by the difference quotient and the derivative lower bound, exhibiting the curve as a local graph; at a corner let $u$ be the outgoing directed unit tangent and $v$ the incoming directed unit tangent. The geometric incident rays point along $u$ and $-v$, so their distinctness excludes $v=-u$. Thus the coordinate $\xi (w)=⟨w,u+v⟩$ has rate $1+⟨u,v⟩>0$ along both branches, so both are $C^1$ graphs over $\xi$ with the corner as common endpoint and disjoint $\xi$-ranges and their union is one local graph, and no opposite-directed tangent case remains under the hypothesis. A small disk about the corner meets the curve in two arcs meeting only at the corner and its complement in that disk has exactly two connected components; every sufficiently short parameter arc has image open in $c(S^1)$, so inside the corresponding ambient open set one chooses an ambient disk in which the curve portion is exactly this local model and whose complement has exactly two connected sides; the finitely many such parameter arcs cover $S^1$, and compactness of $S^1$ yields a finite subcover. Shrink the side rectangles using positive separation of the images of compact nonadjacent parameter arcs; then every overlap near the curve concerns compatible adjacent arc charts and cannot interchange the oriented sides.

The overlap graph of this finite cover is connected, since otherwise the unions of parameter arcs in its two vertex classes would be disjoint nonempty closed subsets covering the connected circle; whenever two parameter arcs overlap, their rectangles overlap near a common curve point and the left-side patches, respectively the right-side patches, meet there because both are the same oriented side of the same local graph, so the unions $V_{+}$ and $V_{-}$ of all left and right patches are connected subsets of the complement and every curve point is approached from each side.

At a smooth edge point $p$ with unit tangent $\tau$ use the oriented coordinate $w=\bar{\tau }(z-p)$: the defining integral is unchanged because $dw\mathrm{/}(w-w_0)=dz\mathrm{/}(z-z_0)$ when $w_0=\bar{\tau }(z_0-p)$, so the local jump lemma [F1] gives different winding numbers on the two side unions near $p$, while the local estimate [F2] makes the winding number constant on each connected side; hence $V_{+}$ and $V_{-}$ lie in two distinct connected components of the complement.

Let $U$ be any component of the open complement; $U$ is closed in the complement by [F4], open in the plane and polygonally connected by [F5], and its boundary is contained in the curve and is nonempty, because otherwise $U$ would be a nonempty proper clopen subset of the connected plane, contradicting [F6]; at a boundary point the local graph patch has exactly two connected sides, and since $U$ meets one of them and an open connected side inside $U$ cannot meet the other, the whole side lies in $U$, identifying $U$ with one of the two global collar-side components; hence the complement has at most two components, and at least two by step 4.1.

The local sides of $V_{+}$ and $V_{-}$ approach every curve point and no component boundary lies off the curve, so the curve is the boundary of both components, and by [F3] exactly one of them is unbounded while the other is bounded; all choices in the collar construction are finite, and neither the Jordan-Brouwer theorem, the Jordan-Schonflies theorem, nor any choice axiom is used.