Cut lemma for minimum spanning trees (source code)

= Cut lemma for minimum spanning trees

Let an <edge> set $F$ be contained in some <minimum spanning tree>, and let a <cut of a graph> have no crossing <edge> in $F$. Any least-weight <edge> crossing that <cut of a graph> can be added to $F$ while preserving its containment in some <minimum spanning tree>. Insert the chosen <edge> into an optimum containing $F$, then remove another crossing <edge> from the resulting <graph cycle>; it is no lighter and cannot belong to $F$. Ties imply existence of an optimum containing the chosen <edge>, rather than membership in every optimum.