:: deftheorem defines alternates_vertices_in GRAPH_2:def 3 :
for G being Graph
for c being FinSequence holds
( c alternates_vertices_in G iff ( len c >= 1 & card (G -VSet (rng c)) = 2 & ( for n being Nat st n in dom c holds
the Source of G . (c . n) <> the Target of G . (c . n) ) ) );