theorem :: GLPACY00:45

for P being _finite non _trivial Path-like _Graph
for v being object
for C being addAdjVertexAll of P,v, Endvertices P st not v in the_Vertices_of P holds
( C is simple & C is Cycle-like )