Minimum spanning tree cut property (source code)

= Minimum spanning tree cut property

The unique lightest <edge> across a <cut of a graph> belongs to every <minimum spanning tree>. If a <spanning tree> omits it, inserting it creates a <graph cycle> with another <edge> across that <cut of a graph>. Removing that heavier <edge> gives a lighter <spanning tree>, a contradiction. This proves the correctness of <Prim algorithm> and <Kruskal algorithm> for distinct weights.