the cycle property

The cut property tells you which cable you can safely add. The cycle property is its mirror image: it tells you which cable you can safely throw away. Look at any closed loop of cables in your network. The single most expensive cable on that loop is never needed — there is always a minimum spanning tree that leaves it out. Whenever you spot a loop, you can delete its heaviest edge with a clear conscience.

Precisely: if an edge e is the unique maximum-weight edge on some cycle, then e is in NO minimum spanning tree. The argument again is an exchange. Suppose some MST T contained e. Removing e splits T into two pieces, cutting the vertices into two sets. The cycle that e lies on must cross between those two pieces using some other edge f (a cycle, broken at e, still connects e's endpoints the long way around). Because e is the heaviest edge on that cycle, weight(f) < weight(e). Swap f in for e: you reconnect the tree with a strictly cheaper edge, producing a spanning tree of smaller total weight — contradicting that T was minimum. So no MST contains e.

The cycle property is the discard rule that complements the cut property's keep rule, and together they justify the greedy MST algorithms completely. Kruskal's algorithm is the cycle property in action: it considers edges from cheapest to most expensive and rejects any edge that would close a cycle, because such an edge is necessarily the heaviest on the cycle it would create. A precise caveat: the clean statement needs the heaviest edge on the cycle to be unique. If several edges on a cycle tie for heaviest, you can drop one of them but not necessarily a specific one, and more than one MST may exist.