Kruskal's greedy edge procedure produces a minimum spanning tree

Maintain the invariant that the current forest $F$ is contained in some MST. It holds initially by L1.

Suppose $F\subseteq T$ for an MST $T$, and Kruskal chooses $e$. If $e\in T$, the invariant persists.

If $e\notin T$, let $C$ be its fundamental cycle in $T+e$. Some edge $f\in E(C)\setminus\{e\}$ is not in $F$; otherwise the $T$-path $C-e$ would lie in $F$ and adding $e$ to $F$ would create a cycle. Since $F+f$ is a subgraph of the acyclic tree $T$, the edge $f$ is eligible for Kruskal.

At the moment $e$ is chosen, $f$ is eligible, so $w(e)\le w(f)$. The exchange $T-f+e$ is a spanning tree of no greater weight, hence an MST containing $F+e$.

Thus the invariant holds after every choice.

On termination, $F$ must be connected: otherwise a path of $G$ between two components of $F$ would contain a first edge joining distinct components, and that edge would still be eligible. Thus $F$ is a spanning tree. The invariant then forces $F$ itself to be an MST.

Therefore every tie-breaking execution returns a minimum spanning tree.