Proof that any algorithm who builds a spanning tree using Cut and Cycle properties is an MST

The Kleinberg and Tardos Algorithm makes the following claim without proof:

Any algorithm that builds a spanning tree by repeatedly including edges when justified by the Cut Property and deleting edges when justified by the Cycle property - in any order at all - will end up with a minimum spanning tree.

Is there any proof for this claim? Intuitively, of course, it seems right. I haven't been able to find a proof however when searching online.

Call the algorithm in that claim CC algorithm.
Assuming all edge costs are distinct

Here is CC algorithm in detail.

Given a weighted connected undirected graph, CC algorithm builds a set of edges by repeating the following step until all edges have been inspected.

• select an arbitrary uninspected edge.

• either it satisfies the Cut property, it will be included in the set.

• or it satisfies the Cycle property, do nothing (i.e., do not include it in the wanted set of edges).

• Mark it as inspected.

Claim 0: There is a unique MST.

Proof: By common knowledge. It is also exercise 8 of chapter "Greedy algorithm", 2005 edition.

Corollary: Every edge either satisfies the Cut property and it is in the unique MST, or it satisfies the Cycle property and it is not in the unique MST.

Claim 1: CC algorithm produces an MST (or, the MST).

Proof: Clearly, CC algorithm includes every edge that satisfies the Cut property and excludes every edge that satisfies the Cycle property. So, it produces the unique MST.

What if all edge costs are not distinct?

Here is CC algorithm in detail, not assuming all edge costs are distinct.

Given a weighted connected undirected graph, CC algorithm builds a set of edges by repeating the following step until all edges have been inspected.

• select an arbitrary uninspected edge.

• if there is some cut such that the edge is the only uninspected edge among all edges that satisfies the Cut property for that cut while no edges included so far satisfy the Cut property for that cut, it will be included.

• else if there is some cut such that the edge satisfies the Cut property for that cut while no edges included so far satisfy the Cut property for that cut, throw a random coin and, include the edge if we get head of the coin.

• Mark the edge as inspected.

That this general version of CC algorithm produces an MST can be proved by mimicking the steps in section "Eliminating the Assumption that All Edge Costs Are Distinct" of that book.

StackExchange Computer Science Q#144542, answer score: 3