for G being finite Graph
for v being Vertex of G
for vs being FinSequence of the carrier of G
for c being Path of G st not c is cyclic & vs is_vertex_seq_of c holds
( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )