To apply the definition in Bondy's textbook, we first have to give the vertices names so we can refer to them:
In the first graph, the external face has boundary $\{ab, ad, bc, cd\}$ and the internal face has boundary $\{ab, ad, bc, be, cd, df\}$, when regarded as edge sets. In the second graph, the external face has boundary $\{ab, ad, bc, be, cd\}$ and the internal face has boundary $\{ab, ad, bc, cd, df\}$. The drawings are not equivalent.
Note that we do not care which order the faces are written in, and which face is external. In a third drawing with both leaves on the outside, the external face would have boundary $\{ab, ad, bc, be, cd, df\}$ and the internal face would have boundary $\{ab, ad, bc, cd\}$. This would be equivalent to the first drawing.
The definition in Bondy's textbook (the edge-set definition) is not equivalent to the homotopy definition. The second example you gave illustrates that. In the edge-set definition, the two embeddings are equivalent: there is only one face, and its boundary is the set of all edges in the graph. (In fact, in the edge-set definition, every tree has a unique embedding.)
There is another combinatorial approach to embedding equivalence. You could call this the face-walk definition. For every face, you write down the closed walk that goes around its boundary in order. For example, for the first graph above, the external face has closed walk $(a,b,c,d,a)$ and the internal face has closed walk $(a,b,e,b,c,d,f,d,a)$. We say that two closed walks are equivalent if we can turn one into the other by possibly choosing a different starting point and/or reversing it, and two embeddings are equivalent if their faces have equivalent closed walks.
This definition distinguishes different embeddings of a tree, and is essentially the same as the homotopy definition. You have to be a bit careful, because as I've stated it, it's not always defined when the graph is not connected, but we can resolve that by allowing a face to have multiple closed walk boundaries.
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.
Best Answer
I don't know for sure what would qualify as a formal proof.
How about: Embed the graph in a sphere (since the polyhedron is convex, choose a sphere whose center is inside the polyhedron; and then radially project vertex points and edge points so that they lie on the sphere); then orient the sphere so that the north pole is not a vertex or on an edge of the embedded graph; and then stereographically project the sphere, along with the embedded graph, onto the horizontal plane through the south pole.