:: deftheorem Def9 defines Rotate GRAPH_3:def 9 :
for G being Graph
for v being Vertex of G
for c being Element of G -CycleSet st v in G -VSet (rng c) holds
Rotate (c,v) = the Element of { c9 where c9 is Element of G -CycleSet : ( rng c9 = rng c & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c9 & vs . 1 = v ) ) } ;