How can we formalise the notion of the face of a planar graph?

I am looking for a way to formalise the notion of the face of a planar graph. I have read through the following links on stack exchange: formal definition of a planar graph, definition of a separating triangle, face of a non-planar graph, notion of a face in graph theory. I also have an introductory graph textbook that only makes passing mention that faces can be defined via a 'generalization of the Jordan curve theorem'. I am trying to formalise these notions in order to formalise (to some extent) another proof that uses graph theory in a very intuitive way. My main issue is I cannot seem to fill in the gaps using the Jordan curve theorem to define a face in a way that deals with every case.

I define a planar graph in the following way: Let $G = (V,E)$ be a graph. We say $G$ is planar if the following hold: (i) there exists an injective function $f: V \rightarrow \mathbb{R}^2$, (ii) for every edge $v_iv_j \in E$, there exists a Jordan arc from $f(v_i)$ to $f(v_j)$, and, no two Jordan arcs intersect except possibly at the image of a vertex under $f$.

Attempt at defining a face: Suppose we have a planar embedding of a planar graph $G$. Suppose there is a closed path of $G$ passing through the vertices $(v,v_1,v_2,...,v_k,v)$. By definition of a planar graph, there are Jordan arcs between $f(v)$ and $f(v_1)$, $f(v_1)$ and $f(v_2)$, etc. The union of all of these Jordan arcs give us a Jordan curve. By the Jordan curve theorem, there is an interior region. If there is no vertex, $v_i$, such that $f(v_i)$ lies in the interior, we call the interior region an interior face of the planar embedding. The exterior face is defined as the plane minus the planar embedding of $G$ and minus all interior faces.

The above definition is verbose, but works in simple cases, like the graph below with two faces.

However, this definition fails for the following two planar embeddings (of the same graph):

Here I do not know how to alter my definition to account for these situations when there is a topological 'line' in what would otherwise be a face.

Can anyone point me to a resource or provide a rigorous definition? In particular I am looking for explicit details, rather than simply knowing that it can be done via the Jordan curve theorem.

To be rigorous, you should not talk about a face of a planar graph, but a face of a planar embedding of a graph, or a face of a plane graph. This is because, as in your example, different embeddings may have different faces.

Here is the definition that I use and that I find in several books that I own: given an embedding $(\phi_e : [0,1] \to \mathbb{R}^2)_{e \in E}$ of a planar graph $(V,E)$, a face is a connected region of $\mathbb{R}^2 \setminus \bigcup_{e \in E} \phi_e([0,1])$.

This is rigorous, but it does not give you much unfortunately. It is not even obvious that the number of faces is finite for instance. The next steps would probably be to prove that if $G$ is connected then each face has a boundary that is a closed walk in $G$, and each edge appears in at most 2 such boundaries, but it also depends on what you want to prove.