+\para
+The Red lemma actually works in both directions and it can be used to characterize
+all non-MST edges, which will turn out to be useful in the latter chapters.
+
+\corn{Cycle rule}\id{cyclerule}%
+An~edge~$e$ is not contained in the MST iff it is the heaviest on some cycle.
+
+\proof
+The implication from the right to the left is the Red lemma. In the other
+direction, when~$e$ is not contained in~$T_{min}$, it is $T_{min}$-heavy (by
+Theorem \ref{mstthm}), so it is the heaviest edge on the cycle $T_{min}[e]+e$.
+\qed
+
+\rem
+The MST problem is a~special case of the problem of finding the minimum basis
+of a~weighted matroid. Surprisingly, when we modify the Red-Blue procedure to
+use the standard definitions of cycles and cuts in matroids, it will always
+find the minimum basis. Some of the other MST algorithms also easily generalize to
+matroids and in some sense matroids are exactly the objects where ``the greedy approach works''. We
+will however not pursue this direction in our work, referring the reader to the Oxley's monograph
+\cite{oxley:matroids} instead.
+