[proofplan] We reduce the edge version of Menger's theorem to the vertex version by encoding edges as vertices. Construct an auxiliary graph $G'$ whose vertex set consists of the edges of $G$ together with two fresh terminal vertices $a', b'$, with adjacency inherited from the line graph of $G$ and terminal edges joining $a'$ (resp.\ $b'$) to every edge of $G$ incident to $a$ (resp.\ $b$). We then show that edges of $G$ separating $a$ from $b$ correspond bijectively to internal vertex separators of $a'$ from $b'$ in $G'$, so the hypothesis $\lambda_{a,b}(G) \geq k$ translates to $\kappa_{a',b'}(G') \geq k$. Applying the [Menger's Theorem (Vertex Version, Local Form)](/theorems/2021) inside $G'$ produces $k$ internally disjoint $a'$–$b'$ paths, which decode to edge-disjoint $a$–$b$ walks in $G$. Each walk contains an $a$–$b$ path by [Walk Contains Path](/theorems/2007), and the edge-disjointness is preserved. [/proofplan]

[step:Construct the auxiliary graph $G'$ by adjoining terminal vertices to the line graph of $G$]Recall that the line graph $L(G)$ has vertex set $E(G)$, with two vertices $e, f \in E(G)$ adjacent in $L(G)$ if and only if $e$ and $f$ share an endpoint in $G$. Define \begin{align*} V(G') &:= E(G) \cup \{a', b'\}, \\ E(G') &:= E(L(G)) \cup \{a'e : e \in E(G), \; a \in e\} \cup \{b'e : e \in E(G), \; b \in e\}, \end{align*} where $a'$ and $b'$ are two fresh vertices not in $E(G)$. Since $a \neq b$ and $G$ is a simple graph, no edge of $G$ is incident to both $a$ and $b$ and a common endpoint simultaneously in a way that would create parallel edges between $a'$ and $b'$; in particular, if $ab \in E(G)$ then this single edge of $G$ is adjacent in $G'$ to both $a'$ and $b'$, but each adjacency is via a different terminal, so $G'$ remains simple. Since $G$ is connected with $a \neq b$, there is at least one edge incident to $a$ (otherwise $a$ is isolated, contradicting connectedness because $|G| \geq 2$), so $\deg_{G'}(a') \geq 1$; likewise $\deg_{G'}(b') \geq 1$.[/step]

[guided]Why reduce to the line graph? The edge version of Menger is about edge-disjoint paths and edge separators, while the vertex version is about internally disjoint paths and vertex separators. The line graph translates "edges of $G$" into "vertices of $G'$", so edge-disjoint structures in $G$ become vertex-disjoint structures in $G'$. This is the standard dualising trick. However, $L(G)$ alone has no natural terminals: the source $a$ and target $b$ are vertices of $G$, not edges. The fix is to manually insert terminal vertices $a'$ and $b'$ into the new graph and attach them to exactly those vertices of $L(G)$ that correspond to edges of $G$ incident to $a$ and $b$, respectively. Concretely: \begin{align*} V(G') &:= E(G) \cup \{a', b'\}, \\ E(G') &:= E(L(G)) \cup \{a'e : e \in E(G), \; a \in e\} \cup \{b'e : e \in E(G), \; b \in e\}. \end{align*} We should verify that $G'$ is a simple graph and that the terminals are well-defined. Suppose $ab \in E(G)$: then the edge $ab$, viewed as a vertex of $G'$, is adjacent to $a'$ (via the first extra set) and to $b'$ (via the second). That is fine — it just means the single edge $ab$ shows up in $G'$ as the common neighbour of $a'$ and $b'$. There is no $a'b'$ edge in $G'$, so simplicity is preserved. We should also verify the terminals are not isolated. If $a$ had no incident edges in $G$, then since $G$ is connected and has at least two vertices (so $a$ lies in a component of size $\geq 2$), $a$ would have a neighbour, contradiction. So $a$ has at least one incident edge in $G$, which means $a'$ has at least one neighbour in $G'$. Symmetrically for $b'$.[/guided]

[step:Translate $a$–$b$ walks in $G$ into $a'$–$b'$ paths in $G'$ and vice versa] [claim:$a'$ is separated from $b'$ in $G'$ by a set $W \subseteq V(G') \setminus \{a', b'\} = E(G)$ if and only if $W$ separates $a$ from $b$ as an edge set in $G$] [proof] Fix $W \subseteq E(G)$. $(\Rightarrow)$ Suppose $W$ does not separate $a$ from $b$ as an edge set in $G$, i.e., there is an $a$–$b$ walk $a = v_0, e_1, v_1, e_2, \ldots, e_m, v_m = b$ in $G$ with $e_i \notin W$ for every $i \in \{1, \ldots, m\}$. By [Walk Contains Path](/theorems/2007), we may assume this is a path (deletion of repeated vertices only removes edges from the walk, keeping the remaining $e_i$ outside $W$). Then \begin{align*} a', \; e_1, \; e_2, \; \ldots, \; e_m, \; b' \end{align*} is a sequence of vertices of $G'$ in which $a'$ is adjacent to $e_1$ (since $a \in e_1$ by construction of $G'$), $e_i$ is adjacent to $e_{i+1}$ in $G'$ for each $i \in \{1, \ldots, m-1\}$ (since $e_i$ and $e_{i+1}$ share the endpoint $v_i$, so they are adjacent in $L(G)$), and $e_m$ is adjacent to $b'$ (since $b \in e_m$). Because the $v_j$ are distinct and each edge $e_i$ has distinct endpoints $\{v_{i-1}, v_i\}$, the vertices $e_1, \ldots, e_m$ are pairwise distinct in $E(G) = V(G') \setminus \{a', b'\}$. Hence this is an $a'$–$b'$ path in $G'$ whose internal vertices all lie outside $W$. So $W$ does not separate $a'$ from $b'$ in $G'$. $(\Leftarrow)$ Conversely, suppose $W$ does not separate $a'$ from $b'$ in $G'$: there is an $a'$–$b'$ path $P'$ in $G'$ whose internal vertices are all in $E(G) \setminus W$. Write \begin{align*} P': \; a', \; e_1, \; e_2, \; \ldots, \; e_m, \; b', \end{align*} with $e_i \in E(G) \setminus W$ for each $i$. By construction of $G'$, the edge $a'e_1$ exists only because $a \in e_1$, so write $e_1 = a u_1$ for some $u_1$; similarly $e_m = u_{m-1} b$ for some $u_{m-1}$. For each $i \in \{1, \ldots, m-1\}$, the edge $e_i e_{i+1}$ in $G'$ comes from $E(L(G))$, meaning $e_i$ and $e_{i+1}$ share an endpoint $v_i \in V(G)$. Write $e_i = v_{i-1} v_i$ consistently (setting $v_0 = a$, $v_m = b$). Then \begin{align*} a = v_0, \; e_1, \; v_1, \; e_2, \; \ldots, \; e_m, \; v_m = b \end{align*} is an $a$–$b$ walk in $G$ whose edges $e_1, \ldots, e_m$ all lie outside $W$. So $W$ does not separate $a$ from $b$ as an edge set in $G$. [/proof] [/claim] [/step]

[step:Apply the vertex version of Menger's theorem inside $G'$]Let $k \geq 1$ and suppose every edge set $W \subseteq E(G)$ separating $a$ from $b$ in $G$ satisfies $|W| \geq k$. By the claim in the previous step, every vertex set $W' \subseteq V(G') \setminus \{a', b'\}$ separating $a'$ from $b'$ in $G'$ satisfies $|W'| \geq k$, i.e., $\kappa_{a', b'}(G') \geq k$. Observe that $a' b' \notin E(G')$: there are no edges in $E(G')$ incident to both $a'$ and $b'$ by construction (the only edges at $a'$ join it to elements of $E(G)$ incident to $a$; those are vertices of $G'$ distinct from $b'$). So the vertex version of Menger's theorem applies directly. By [Menger's Theorem (Vertex Version, Local Form)](/theorems/2021) applied in $G'$ to the non-adjacent vertices $a', b'$, there exist $k$ internally disjoint $a'$–$b'$ paths $P'_1, \ldots, P'_k$ in $G'$.[/step]

[guided]We want to invoke the local vertex version of Menger's theorem on $a', b'$ in $G'$. That theorem has two hypotheses to check: (i) $a'$ and $b'$ are non-adjacent in $G'$, and (ii) every $a'$–$b'$ separator in $G'$ has size at least $k$. For (i): by the construction in Step 1, the edges incident to $a'$ are exactly $\{a'e : e \in E(G), a \in e\}$, each of which joins $a'$ to a vertex of $G'$ that lies in $E(G) \subseteq V(G') \setminus \{a', b'\}$. There is no edge joining $a'$ to $b'$. So $a' \not\sim b'$ in $G'$. For (ii): the previous step's claim shows that a subset $W \subseteq V(G') \setminus \{a', b'\} = E(G)$ is an $a'$–$b'$ separator in $G'$ if and only if it is an $a$–$b$ edge separator in $G$. By hypothesis, every $a$–$b$ edge separator in $G$ has size at least $k$. Therefore every $a'$–$b'$ vertex separator in $G'$ (avoiding $a', b'$) has size at least $k$, i.e., $\kappa_{a', b'}(G') \geq k$. Both hypotheses are met, so the local vertex version of Menger's theorem gives $k$ internally disjoint $a'$–$b'$ paths $P'_1, \ldots, P'_k$ in $G'$. "Internally disjoint" means the paths pairwise share no internal vertices — equivalently, no vertex of $E(G)$ lies on two of the $P'_j$.[/guided]

[step:Decode each $a'$–$b'$ path into an edge-disjoint $a$–$b$ walk in $G$ and extract paths]Fix $j \in \{1, \ldots, k\}$ and write $P'_j$ explicitly: \begin{align*} P'_j: \; a', \; e_1^{(j)}, \; e_2^{(j)}, \; \ldots, \; e_{m_j}^{(j)}, \; b', \end{align*} with $e_1^{(j)}, \ldots, e_{m_j}^{(j)} \in E(G)$ pairwise distinct (as $P'_j$ is a path). By the decoding in Step 2's claim, there is an $a$–$b$ walk $W_j$ in $G$ using exactly the edges $e_1^{(j)}, \ldots, e_{m_j}^{(j)}$, in that order. We check edge-disjointness of the walks $W_1, \ldots, W_k$. The edges of $W_j$ are exactly the internal vertices of $P'_j$. Since the $P'_j$ are internally disjoint in $G'$, for any $j \neq j'$ and any $i, i'$, the internal vertices $e_i^{(j)}$ and $e_{i'}^{(j')}$ of $P'_j$ and $P'_{j'}$ respectively are distinct elements of $V(G') \setminus \{a', b'\} = E(G)$. Hence $W_j$ and $W_{j'}$ use disjoint edge sets of $G$. Finally, by [Walk Contains Path](/theorems/2007), each walk $W_j$ contains an $a$–$b$ path $Q_j$ as a sub-sequence; in particular, $E(Q_j) \subseteq E(W_j) = \{e_1^{(j)}, \ldots, e_{m_j}^{(j)}\}$. Edge-disjointness of the $W_j$ therefore passes to edge-disjointness of the $Q_j$: \begin{align*} E(Q_j) \cap E(Q_{j'}) \subseteq E(W_j) \cap E(W_{j'}) = \varnothing \quad \text{for } j \neq j'. \end{align*} This produces $k$ edge-disjoint $a$–$b$ paths $Q_1, \ldots, Q_k$ in $G$, completing the proof.[/step]

[guided]We decode the paths $P'_j$ back into structures in $G$. Each $P'_j$ has the shape \begin{align*} a', \; e_1^{(j)}, \; e_2^{(j)}, \; \ldots, \; e_{m_j}^{(j)}, \; b', \end{align*} and by the encode/decode correspondence of Step 2 the sequence $e_1^{(j)}, \ldots, e_{m_j}^{(j)}$ is the edge sequence of an $a$–$b$ walk $W_j$ in $G$. Why walks and not paths directly? In general the line graph encoding preserves the edge sequence but not necessarily vertex-uniqueness in $G$: a walk in $G$ can revisit vertices without revisiting edges, and this would still correspond to a simple path in $G'$. So we only get walks at this stage. Are the walks edge-disjoint? Suppose for contradiction that some edge $e \in E(G)$ appears in both $W_j$ and $W_{j'}$ for some $j \neq j'$. Then $e$ is listed as an internal vertex of both $P'_j$ and $P'_{j'}$. But the paths $P'_1, \ldots, P'_k$ are internally disjoint, so no vertex of $V(G') \setminus \{a', b'\}$ lies on two of them — contradiction. Hence edge-disjointness holds. Finally, we need edge-disjoint paths, not just walks. By [Walk Contains Path](/theorems/2007), every $a$–$b$ walk in $G$ contains an $a$–$b$ path using only edges of the walk. Extracting such a path $Q_j$ from each $W_j$ yields paths whose edge sets are subsets of the original disjoint edge sets, so the $Q_j$ are also pairwise edge-disjoint. This gives the $k$ edge-disjoint $a$–$b$ paths required.[/guided]