[proofplan] The strategy parallels the general planar edge bound: reduce to the connected case, establish a lower bound on face degrees via double counting, then combine with [Euler's Formula](/theorems/2014). The key difference is that the triangle-free hypothesis forces every face-boundary closed walk to have length at least $4$ rather than $3$: a face of degree $3$ would be bounded by a $3$-cycle (a triangle), which is forbidden. This strengthens $3F \le 2e(G)$ to $4F \le 2e(G)$, and substituting $F = 2 - |G| + e(G)$ from Euler's formula yields the sharper bound $e(G) \le 2(|G| - 2)$. [/proofplan] [step:Reduce to the case where $G$ is connected and triangle-free] Let $G$ be a planar graph with $n := |G| \ge 4$ containing no cycle of length $3$. If $G$ is disconnected, we may add edges between distinct components while preserving both planarity and the triangle-free property: at each step, pick two distinct components $G_1, G_2$ and a pair of vertices $u \in V(G_1), v \in V(G_2)$, and add the edge $\{u, v\}$. Since $u$ and $v$ previously had no common neighbour (they lay in different components, sharing no vertex), the new edge creates no triangle. The process preserves planarity (a cross-component edge can be drawn without crossings using the unbounded face), and at each step $e(G)$ strictly increases. After finitely many steps, the graph is connected. The target inequality $e(G) \le 2(n - 2)$ only becomes stronger under edge addition, so it suffices to prove the bound for the connected triangle-free supergraph. Hence, without loss of generality, assume $G$ is connected and triangle-free. Fix a planar embedding and write $m := e(G)$, $F$ for the face count. [guided] Two things deserve emphasis in this reduction. First, the triangle-free property is preserved under cross-component edge additions because a triangle needs three mutually adjacent vertices, and those must all lie in the same component; adding an edge between components cannot create a new triangle. Second, the reduction is strictly to our benefit: the bound $e(G) \le 2(n - 2)$ is an upper bound on $e(G)$, and proving it for a larger connected graph implies it for the original disconnected graph. The hypothesis $n \ge 4$ is the correct minimum: for $n = 3$, a triangle-free simple graph on $3$ vertices has at most $2$ edges (the graph $P_3$, a path of length $2$), and the target bound gives $2(3 - 2) = 2$, which matches — so the theorem also holds for $n = 3$. For $n \le 2$, the bound $2(n - 2) \le 0$ would force $e(G) \le 0$, which is automatic. The cutoff $n \ge 4$ in the theorem statement guarantees that the face-degree bound $\deg(f) \ge 4$ is non-vacuous (for $n \ge 4$ there exist connected triangle-free planar graphs with at least one face). [/guided] [/step] [step:Bound each face degree below by $4$ using the triangle-free hypothesis] For each face $f$ of the embedding, define \begin{align*} \deg(f) := \#\{\text{edge-sides incident to } f\} = \text{length of the boundary closed walk of } f. \end{align*} We claim $\deg(f) \ge 4$ for every face $f$. By the argument in the general planar edge bound, in a simple connected plane graph with $n \ge 3$ vertices, $\deg(f) \ge 3$. So we only need to rule out $\deg(f) = 3$. Suppose for contradiction that some face $f$ has $\deg(f) = 3$. The boundary closed walk of $f$ has length $3$. Since $G$ is simple (no loops, no multi-edges), a closed walk of length $3$ must visit three distinct vertices $x_1, x_2, x_3$ with edges $\{x_1, x_2\}, \{x_2, x_3\}, \{x_3, x_1\}$ — i.e., a $3$-cycle (triangle) in $G$. This contradicts the triangle-free hypothesis. Therefore $\deg(f) \ge 4$ for every face $f$. [guided] The step that upgrades the bound from $\deg(f) \ge 3$ (generic planar case) to $\deg(f) \ge 4$ (triangle-free case) is the crux. In a simple graph, a closed walk of length $3$ must be a triangle: \begin{itemize} \item Length $1$ requires a loop — forbidden in simple graphs. \item Length $2$ requires a multi-edge (two parallel edges between two vertices) — forbidden in simple graphs. \item Length $3$ can only be the closed walk $x_1, x_2, x_3, x_1$ with all three vertices distinct (otherwise we would repeat an edge, violating the walk being a closed walk that traces the boundary of a face on both sides) — hence a $3$-cycle. \end{itemize} So $\deg(f) = 3$ is possible only when a $3$-cycle bounds the face. The triangle-free hypothesis removes this possibility, forcing $\deg(f) \ge 4$. Why, in a triangle-free simple graph, does the minimum face-boundary length jump from $3$ to $4$ rather than, say, to $5$? Because length $4$ is achievable — the $4$-cycle $C_4$ is a triangle-free plane graph with a face of degree $4$. Any stronger lower bound would fail in the example $C_4$ itself. [/guided] [/step] [step:Double-count edge–face incidences to get $4F \le 2e(G)$] Summing the face degrees, \begin{align*} \sum_{f} \deg(f) = 2 e(G), \end{align*} by the double-counting identity: each edge has exactly two sides, and each side lies on the boundary of exactly one face, so each edge contributes exactly $2$ to the total. Combining with $\deg(f) \ge 4$ from the previous step: \begin{align*} 4 F \le \sum_{f} \deg(f) = 2 e(G), \end{align*} hence \begin{align*} F \le \frac{e(G)}{2} = \frac{m}{2}. \end{align*} [guided] The double-counting identity $\sum_f \deg(f) = 2m$ holds for any plane multigraph; it was established in the general planar edge bound by counting edge-face incidence pairs two ways. The upgrade in this theorem comes entirely from the stronger face-degree bound: $4F \le \sum_f \deg(f)$ replaces the generic $3F \le \sum_f \deg(f)$, and dividing by the coefficient on the left gives $F \le m/2$ rather than $F \le 2m/3$. Notice that the bound $F \le m/2$ is sharp: equality holds when every face has degree exactly $4$, which occurs for planar **quadrangulations** (simple planar graphs all of whose faces are $4$-cycles). For such graphs, the upper bound $e(G) = 2(n - 2)$ is attained. [/guided] [/step] [step:Apply Euler's formula and rearrange to $e(G) \le 2(|G| - 2)$] Since $G$ is a connected plane graph, by [Euler's Formula](/theorems/2014): \begin{align*} n - m + F = 2, \qquad \text{i.e.,} \qquad F = 2 - n + m. \end{align*} Substituting into the bound $F \le m/2$: \begin{align*} 2 - n + m \le \frac{m}{2}. \end{align*} Multiply through by $2$: \begin{align*} 4 - 2n + 2m \le m. \end{align*} Rearranging: \begin{align*} m \le 2n - 4 = 2(n - 2). \end{align*} Since $n = |G|$ and $m = e(G)$, this is $e(G) \le 2(|G| - 2)$, which is the desired bound. [guided] The final algebra is identical in structure to the general planar edge bound but uses the tighter constant. Euler's formula eliminates the embedding-dependent quantity $F$, and the triangle-free double-counting bound $F \le m/2$ (as opposed to $F \le 2m/3$ in the generic case) propagates through the rearrangement to give $m \le 2n - 4$ rather than $m \le 3n - 6$. The sharpness claim is worth noting: the bound $e(G) \le 2(n - 2)$ is attained by the complete bipartite graph $K_{2,2} = C_4$ on $n = 4$ vertices with $m = 4 = 2 \cdot 2$ edges, and more generally by all planar quadrangulations. In particular, $K_{3,3}$ — if it were planar — would have $n = 6$, $m = 9 > 2 \cdot 4 = 8$, violating this bound; hence $K_{3,3}$ is not planar. This is one of the two classical non-planarity arguments (the other uses $K_5$ and the general bound $e \le 3n - 6$). [/guided] [/step]