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
{ 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 ) ) } is non empty Subset of (G -CycleSet)