Solution (source code)

= Solution

For a closed <Eulerian trail>, every visit to a <vertex> pairs one entering <edge> with one departing <edge>, including the initial/final <vertex>. Thus every <degree of a vertex>[degree] is even.

Conversely, in a finite <connected graph> with all degrees even, start at a <vertex> and follow unused <edges> until no extension is possible. The walk cannot stop away from its starting point: at a different endpoint an odd number of its incident <edges> would have been used, leaving at least one unused <edge> because its total <degree of a vertex>[degree] is even. Thus it closes. If any <edge> remains unused, <connectedness> gives a <vertex> of the current closed trail incident with an unused <edge>. Repeat the construction from that <vertex> in the unused-<edge> subgraph and splice the resulting closed trail into the first one. Finitely many <edges> make the procedure terminate in a closed trail using every <edge> exactly once.

Hence \b[a <connected> finite <graph> has an Eulerian circuit exactly when all degrees are even]. If “trail” is allowed to be open, the printed equivalence needs correction: a <connected graph> has an <Eulerian trail> when it has zero or two odd-<degree of a vertex>[degree] <vertices>. A single <edge> is an immediate counterexample to the unqualified printed statement.