for G being connected finite Graph
for c being Element of G -CycleSet st rng c <> the carrier' of G & not c is empty holds
{ v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } is non empty Subset of the carrier of G