Cycles in a graph via the DFS tree

Lemma

A directed graph has a cycle if and only if its DFS tree has a back edge.

Proof

Suppose we have a graph and some run of a DFS algorithm that forms DFS tree .

Suppose it has some cycle where and . Then some vertex must have been discovered first by .

All other vertices must be below and contained in its branch. Therefore is contained in its branch with edge giving the desired back edge.

Suppose we have some back edge . By the definition of back edge but and are in the same branch in .

Therefore there are edges connecting to in making a cycle.