for G being connected finite Graph holds
( ex p being Path of G st
( not p is cyclic & p is Eulerian ) iff ex v1, v2 being Vertex of G st
( v1 <> v2 & ( for v being Vertex of G holds
( Degree v is even iff ( v <> v1 & v <> v2 ) ) ) ) )