:: deftheorem Def12 defines -CycleSet GRAPH_3:def 12 :
for G being finite Graph
for v being Vertex of G
for X being set st ( for v being Vertex of G holds Degree (v,X) is even ) & Degree (v,X) <> 0 holds
X -CycleSet v = { c where c is Element of G -CycleSet : ( rng c c= X & not c is empty & ex vs being FinSequence of the carrier of G st
( vs is_vertex_seq_of c & vs . 1 = v ) ) } ;