 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.