let C be simple Cycle-like _Graph; :: thesis:
let v be Vertex of C; :: thesis:
set P = the removeVertex of C,v;
A1: not C is _trivial ;
then A2: the removeVertex of C,v is Path-like by Th54;
not the removeVertex of C,v is _trivial

proof

assume the removeVertex of C,v is _trivial ; :: thesis:
then A4: the removeVertex of C,v .order() = 1 by GLIB_000:26;
C .order() = ( the removeVertex of C,v .order()) + 1 by A1, GLIB_000:48;
then C is 0 + 2 -vertex by A4, GLIB_013:def 3;
hence contradiction ; :: thesis:

end;

then reconsider P = the removeVertex of C,v as non _trivial Path-like _Graph by A2;
take P ; :: thesis:
A5: the_Vertices_of P = (the_Vertices_of C) \ {v} by A1, GLIB_000:47;
hence A6: not v in the_Vertices_of P by ZFMISC_1:56; :: thesis:
A7: C is Supergraph of P by GLIB_006:57;
A8: the_Edges_of P = C .edgesBetween ((the_Vertices_of C) \ {v}) by A1, GLIB_000:47;

now :: thesis:

thus the_Vertices_of C = (the_Vertices_of P) \/ {v} by A5, ZFMISC_1:116; :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
thus A10: not e Joins v,v,C by GLIB_000:18; :: thesis:
let v1 be object ; :: thesis:

hereby :: thesis:

assume A11: ( not v1 in Endvertices P & e Joins v1,v,C ) ; :: thesis:
then reconsider v1 = v1 as Vertex of C by GLIB_000:13;
v <> v1 by A10, A11;
then reconsider v2 = v1 as Vertex of P by A5, ZFMISC_1:56;
v2 .degree() <= 2 by Th17;
then not not v2 .degree() = 0 & ... & not v2 .degree() = 2 ;

per cases ;

suppose v2 .degree() = 0 ; :: thesis:

hence contradiction by GLIB_000:def 50; :: thesis:

end;

suppose v2 .degree() = 1 ; :: thesis:

hence contradiction by A11, GLIB_006:56, GLIB_000:def 52; :: thesis:

end;

suppose v2 .degree() = 2 ; :: thesis:

then card (v2 .allNeighbors()) = 2 by GLIB_000:111;
then consider x, y being object such that
A14: ( x <> y & v2 .allNeighbors() = {x,y} ) by CARD_2:60;

now :: thesis:

let z be object ; :: thesis:
assume z in {x,y,v} ; :: thesis:

per cases by ENUMSET1:def 1;

suppose ( z = x or z = y ) ; :: thesis:

then A15: z in v2 .allNeighbors() by A14, TARSKI:def 2;
v2 .allNeighbors() c= v1 .allNeighbors() by GLIB_000:82;
hence z in v1 .allNeighbors() by A15; :: thesis:

end;

suppose z = v ; :: thesis:

hence z in v1 .allNeighbors() by A11, GLIB_000:71; :: thesis:

end;

then card {x,y,v} c= card (v1 .allNeighbors()) by TARSKI:def 3, CARD_1:11;
then A16: card {x,y,v} c= v1 .degree() by GLIB_000:111;
( v <> x & v <> y )

proof

( x in v2 .allNeighbors() & y in v2 .allNeighbors() ) by A14, TARSKI:def 2;
hence ( v <> x & v <> y ) by A5, ZFMISC_1:56; :: thesis:

end;

then 3 c= v1 .degree() by A14, A16, CARD_2:58;
then Segm 3 c= Segm 2 by GLIB_016:def 4;
hence contradiction by NAT_1:39; :: thesis:

end;

let v2 be object ; :: thesis:
assume A17: ( v1 <> v & v2 <> v & e DJoins v1,v2,C ) ; :: thesis:
then A18: e Joins v1,v2,C by GLIB_000:16;
then ( v1 in the_Vertices_of C & v2 in the_Vertices_of C ) by GLIB_000:13;
then ( v1 in (the_Vertices_of C) \ {v} & v2 in (the_Vertices_of C) \ {v} ) by A17, ZFMISC_1:56;
then A19: e in the_Edges_of P by A8, A18, GLIB_000:32;
( e is set & v1 is set & v2 is set ) by TARSKI:1;
hence e DJoins v1,v2,P by A17, A19, GLIB_000:73; :: thesis:

end;

thus ex E being set st
( card (Endvertices P) = card E & E misses the_Edges_of P & the_Edges_of C = (the_Edges_of P) \/ E & ( for v1 being object st v1 in Endvertices P holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,C & ( for e2 being object st e2 Joins v1,v,C holds
e1 = e2 ) ) ) ) :: thesis:

proof

take E = v .edgesInOut() ; :: thesis:
consider P0 being vertex-distinct Path of P such that
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P ) and
A20: ( Endvertices P = {(P0 .first()),(P0 .last())} iff not P is _trivial ) and
( P0 is trivial iff P is _trivial ) and
A21: ( P0 is closed iff P is _trivial ) and
P0 is minlength by Th31;
A22: P0 .first() <> P0 .last() by A21, GLIB_001:def 24;
thus card (Endvertices P) = 2 by A20, A22, CARD_2:57
.= v .degree() by GLIB_016:def 4
.= card E by GLIB_000:19 ; :: thesis:
thus E misses the_Edges_of P :: thesis:

proof

assume E meets the_Edges_of P ; :: thesis:
then consider x being object such that
A23: ( x in E & x in the_Edges_of P ) by XBOOLE_0:3;
consider w being Vertex of C such that
A24: x Joins v,w,C by A23, GLIB_000:64;
x Joins v,w,P by A23, A24, GLIB_000:73;
then v in the_Vertices_of P by GLIB_000:13;
hence contradiction by A5, ZFMISC_1:56; :: thesis:

end;

for x being object holds
( x in the_Edges_of C iff ( x in the_Edges_of P or x in E ) )

proof

let x be object ; :: thesis:
thus ( not x in the_Edges_of C or x in the_Edges_of P or x in E ) :: thesis:

proof

assume A25: x in the_Edges_of C ; :: thesis:
set w1 = (the_Source_of C) . x;
set w2 = (the_Target_of C) . x;
A26: x Joins (the_Source_of C) . x,(the_Target_of C) . x,C by A25, GLIB_000:def 13;
then reconsider w1 = (the_Source_of C) . x, w2 = (the_Target_of C) . x as Vertex of C by GLIB_000:13;
reconsider x = x as set by TARSKI:1;

per cases ;

suppose ( w1 = v or w2 = v ) ; :: thesis:

then ( x Joins v,w2,C or x Joins v,w1,C ) by A26, GLIB_000:14;
hence ( x in the_Edges_of P or x in E ) by GLIB_000:64; :: thesis:

end;

suppose ( w1 <> v & w2 <> v ) ; :: thesis:

then ( w1 in (the_Vertices_of C) \ {v} & w2 in (the_Vertices_of C) \ {v} ) by ZFMISC_1:56;
hence ( x in the_Edges_of P or x in E ) by A8, A26, GLIB_000:32; :: thesis:

end;

assume ( x in the_Edges_of P or x in E ) ; :: thesis:

per cases ;

suppose A28: x in the_Edges_of P ; :: thesis:

the_Edges_of P c= the_Edges_of C by GLIB_000:def 32;
hence x in the_Edges_of C by A28; :: thesis:

end;

suppose x in E ; :: thesis:

hence x in the_Edges_of C ; :: thesis:

end;

hence the_Edges_of C = (the_Edges_of P) \/ E by XBOOLE_0:def 3; :: thesis:
let v1 be object ; :: thesis:
assume A29: v1 in Endvertices P ; :: thesis:
then reconsider w1 = v1 as Vertex of P ;
reconsider w2 = w1 as Vertex of C by A5, XBOOLE_0:def 5;
take e1 = the Element of (w2 .edgesInOut()) \ (w1 .edgesInOut()); :: thesis:
(w2 .edgesInOut()) \ (w1 .edgesInOut()) <> {}

proof

A30: card (w2 .edgesInOut()) = w2 .degree() by GLIB_000:19
.= 2 by GLIB_016:def 4 ;
consider e0 being object such that
A31: ( w1 .edgesInOut() = {e0} & not e0 Joins w1,w1,P ) by A29, GLIB_000:def 51, GLIB_006:56;
A32: card (w1 .edgesInOut()) = 1 by A31, CARD_1:30;
1 in 2 by CARD_1:50, TARSKI:def 2;
hence (w2 .edgesInOut()) \ (w1 .edgesInOut()) <> {} by A30, A32, CARD_1:68; :: thesis:

end;

then A33: ( e1 in w2 .edgesInOut() & not e1 in w1 .edgesInOut() ) by XBOOLE_0:def 5;
then consider u being Vertex of C such that
A34: e1 Joins w2,u,C by GLIB_000:64;
A35: u = v

proof

assume u <> v ; :: thesis:
then A36: u in (the_Vertices_of C) \ {v} by ZFMISC_1:56;
then A37: e1 in the_Edges_of P by A5, A8, A34, GLIB_000:32;
e1 Joins w1,u,P by A34, A37, GLIB_000:73;
then e1 in w1 .edgesInOut() by A5, A36, GLIB_000:64;
hence contradiction by A33; :: thesis:

end;

hence e1 in E by A34, GLIB_000:14, GLIB_000:64; :: thesis:
thus ( e1 Joins v1,v,C & ( for e2 being object st e2 Joins v1,v,C holds
e1 = e2 ) ) by A34, A35, GLIB_000:def 20; :: thesis:

end;

hence C is addAdjVertexAll of P,v, Endvertices P by A6, A7, GLIB_007:def 4; :: thesis: