:: deftheorem Def13 defines ExtendCycle GRAPH_3:def 13 :
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
for b₃ being Element of G -CycleSet holds
( b₃ = ExtendCycle c iff ex c9 being Element of G -CycleSet ex v being Vertex of G st
( v = the Element of { v9 where v9 is Vertex of G : ( v9 in G -VSet (rng c) & Degree v9 <> Degree (v9,(rng c)) ) } & c9 = the Element of ( the carrier' of G \ (rng c)) -CycleSet v & b₃ = CatCycles (c,c9) ) );