let C be 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} )
let v1, v2 be 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} )
let e be Edge of C; ( e DJoins v1,v2,C implies 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} ) )
assume A1:
e DJoins v1,v2,C
; 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} )
then A2:
( v1 = (the_Source_of C) . e & v2 = (the_Target_of C) . e & e in the_Edges_of C )
by GLIB_000:def 14;
take P = the removeEdge of C,e; ( not e in the_Edges_of P & C is addEdge of P,v1,e,v2 & Endvertices P = {v1,v2} )
the_Edges_of P = (the_Edges_of C) \ {e}
by GLIB_000:51;
hence A3:
not e in the_Edges_of P
by ZFMISC_1:56; ( C is addEdge of P,v1,e,v2 & Endvertices P = {v1,v2} )
reconsider w1 = v1, w2 = v2 as Vertex of P by GLIB_000:def 33;
thus
C is addEdge of P,v1,e,v2
by A2, GLIB_008:37; Endvertices P = {v1,v2}
then A4:
C is addEdge of P,w1,e,w2
;
A5:
v1 <> v2
by A1, GLIB_000:136;
1 + 1 =
v1 .degree()
by GLIB_016:def 4
.=
(w1 .degree()) +` 1
by A3, A4, A5, GLIBPRE0:47
;
then
w1 is endvertex
by GLIB_000:174;
then A6:
w1 in Endvertices P
by GLIB_006:56;
1 + 1 =
v2 .degree()
by GLIB_016:def 4
.=
(w2 .degree()) +` 1
by A3, A4, A5, GLIBPRE0:48
;
then
w2 in Endvertices P
by GLIB_000:174, GLIB_006:56;
then A7:
{w1,w2} c= Endvertices P
by A6, ZFMISC_1:32;
consider x, y being Vertex of P such that
A8:
( x <> y & Endvertices P = {x,y} )
by Th36;
( ( w1 = x or w1 = y ) & ( w2 = x or w2 = y ) )
by A7, A8, ZFMISC_1:22;
hence
Endvertices P = {v1,v2}
by A5, A8; verum