:: deftheorem defines Eulerian GRAPH_3:def 14 :
for G being Graph
for p being Path of G holds
( p is Eulerian iff rng p = the carrier' of G );