theorem Th45: :: GLPACY00:37

for C being non _trivial Cycle-like _Graph
for v1, v2 being Vertex of C
for e being Edge of C st e DJoins v1,v2,C holds
ex P being _finite non _trivial Path-like _Graph st
( not e in the_Edges_of P & C is addEdge of P,v1,e,v2 & Endvertices P = {v1,v2} )