Statement: Any digraph that contains a closed directed walk of length at least one contains a directed cycle
Is the proof as simple as using the definition of a closed walk? A walk is closed if the starting vertex is the same as the ending vertex. Therefore a closed directed walk of length at least one is a directed cycle of length one.
No. Directed closed walks can reuse edges and vertices, directed cycles may not.
However, it's still not a difficult proof. Since there are directed close walks, by the well-ordering of the natural numbers we may choose a directed closed walk of minimal length. This could not have any duplicated vertices, because otherwise we could cut out the overlap and make a shorter directed closed walk. Therefore, that minimal length directed closed walk must be a directed cycle.