theorem Th57: :: GRAPH_3:57

for G being connected finite Graph
for c being Element of G -CycleSet st rng c <> the carrier' of G & not c is empty & ( for v being Vertex of G holds Degree v is even ) holds
( not ExtendCycle c is empty & card (rng c) < card (rng (ExtendCycle c)) )