Solution (source code)

= Solution

The <minimum spanning tree cut property>, in its safe-edge form, says: if an edge set $A$ is contained in some <minimum spanning tree>, a <cut of a graph> respects $A$, and $e$ is a <light edge crossing a cut>, then $A\cup\{e\}$ is contained in some <minimum spanning tree>.

Choose an <MST> $T$ containing $A$. If $e\in T$, nothing changes. Otherwise adding $e$ creates its unique <fundamental cycle>. The path in $T$ between the endpoints of $e$ must cross the chosen cut; take such an edge $f$. Since the cut respects $A$, $f\notin A$. Since $e$ is light, $w(e)\leq w(f)$. The exchange $T-f+e$ is a <spanning tree> containing $A\cup\{e\}$, with total weight no greater than that of $T$. Minimality of $T$ forces equal optimum weight, proving the claim. Equal edge weights cause no difficulty: “safe” means belonging to some compatible optimum, not to every optimum.