let P be _finite non _trivial Path-like _Graph; :: thesis: for v1, v2 being Element of Endvertices P
for e being object
for C being addEdge of P,v1,e,v2 st v1 <> v2 & not e in the_Edges_of P holds
C is Cycle-like
let v1, v2 be Element of Endvertices P; :: thesis: for e being object
for C being addEdge of P,v1,e,v2 st v1 <> v2 & not e in the_Edges_of P holds
C is Cycle-like
let e be object ; :: thesis: for C being addEdge of P,v1,e,v2 st v1 <> v2 & not e in the_Edges_of P holds
C is Cycle-like
let C be addEdge of P,v1,e,v2; :: thesis: ( v1 <> v2 & not e in the_Edges_of P implies C is Cycle-like )
assume A1: ( v1 <> v2 & not e in the_Edges_of P ) ; :: thesis: C is Cycle-like
A2: card (Endvertices P) = 2 by Th37;
then A3: Endvertices P <> {} ;
then reconsider v1 = v1, v2 = v2 as Vertex of P by TARSKI:def 3;
A4: C is addEdge of P,v1,e,v2 ;
A5: ( v1 is endvertex & v2 is endvertex ) by A3, GLIB_006:56;

now :: thesis: for v being Vertex of C holds v .degree() = 2

let v be Vertex of C; :: thesis: b₁ .degree() = 2
reconsider w = v as Vertex of P by A4, GLIB_006:102;

per cases ( ( w <> v1 & w <> v2 ) or w = v1 or w = v2 ) ;

suppose A6: ( w <> v1 & w <> v2 ) ; :: thesis: b₁ .degree() = 2

A7: not w is endvertex

proof

assume w is endvertex ; :: thesis: contradiction
then ( w in Endvertices P & v1 in Endvertices P & v2 in Endvertices P ) by A3, GLIB_006:def 8;
then card {w,v1,v2} c= card (Endvertices P) by NOMIN_2:1, CARD_1:11;
then 3 c= card (Endvertices P) by A1, A6, CARD_2:58;
then A8: {0,1,2} c= 2 by Th37, CARD_1:51;
2 in {0,1,2} by ENUMSET1:def 1;
then 2 in 2 by A8;
hence contradiction ; :: thesis: verum

end;

thus v .degree() = w .degree() by A6, GLIBPRE0:46
.= 2 by A7, Th35 ; :: thesis: verum

end;

suppose w = v1 ; :: thesis: b₁ .degree() = 2

hence v .degree() = (v1 .degree()) +` 1 by A1, A4, GLIBPRE0:47
.= 1 +` 1 by A5, GLIB_000:174
.= 2 ;
:: thesis: verum

end;

suppose w = v2 ; :: thesis: b₁ .degree() = 2

hence v .degree() = (v2 .degree()) +` 1 by A1, A4, GLIBPRE0:48
.= 1 +` 1 by A5, GLIB_000:174
.= 2 ;
:: thesis: verum

end;

end;

end;

then A9: C is 2 -regular by GLIB_016:def 4;
A10: e DJoins v1,v2,C by A1, GLIB_006:105;

now :: thesis: ex C0 being Walk of C st C0 is Cycle-like

consider P0 being vertex-distinct Path of P such that
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P ) and
A11: ( Endvertices P = {(P0 .first()),(P0 .last())} iff not P is _trivial ) and
A12: ( P0 is trivial iff P is _trivial ) and
A13: ( P0 is closed iff P is _trivial ) and
P0 is minlength by Th31;
reconsider P9 = P0 as Walk of C by GLIB_006:75;
take C0 = P9 .addEdge e; :: thesis: b₁ is Cycle-like
A14: e Joins P9 .last() ,P9 .first() ,C

proof

( ( v1 = P0 .first() or v1 = P0 .last() ) & ( v2 = P0 .first() or v2 = P0 .last() ) ) by A11, TARSKI:def 2;

per cases then ( ( v1 = P0 .first() & v2 = P0 .last() ) or ( v1 = P0 .last() & v2 = P0 .first() ) ) by A1;

suppose ( v1 = P0 .first() & v2 = P0 .last() ) ; :: thesis: e Joins P9 .last() ,P9 .first() ,C

hence e Joins P9 .last() ,P9 .first() ,C by A10, GLIB_000:16; :: thesis: verum

end;

suppose ( v1 = P0 .last() & v2 = P0 .first() ) ; :: thesis: e Joins P9 .last() ,P9 .first() ,C

hence e Joins P9 .last() ,P9 .first() ,C by A10, GLIB_000:16; :: thesis: verum

end;

end;

end;

3 <= len P9 by A12, GLIB_001:125;

per cases then ( 3 < len P9 or 3 = len P9 ) by XXREAL_0:1;

suppose A15: 3 < len P9 ; :: thesis: b₁ is Cycle-like

P is Subgraph of C by GLIB_006:57;
then A16: P9 is Path-like by GLIB_001:176;
P9 is open by A13, GLIB_001:121;
hence C0 is Cycle-like by A14, A15, A16, CHORD:33; :: thesis: verum

end;

suppose A17: 3 = len P9 ; :: thesis: b₁ is Cycle-like

then consider e0 being object such that
A18: e0 Joins P0 .first() ,P0 .last() ,P and
A19: P0 = P .walkOf ((P0 .first()),e0,(P0 .last())) by GLIBPRE1:28;
C0 .first() = P9 .first() by A14, GLIB_001:63
.= C0 .last() by A14, GLIB_001:63 ;
then A21: C0 is closed by GLIB_001:def 24;
A22: len C0 = (len P9) + 2 by A14, GLIB_001:64
.= 5 by A17 ;
then A23: C0 is trivial by GLIB_001:126;
A24: C0 is Trail-like

proof

A25: C0 .edgeSeq() = (P9 .edgeSeq()) ^ <*e*> by A14, GLIB_001:82
.= (P0 .edgeSeq()) ^ <*e*> by GLIB_001:86
.= <*e0*> ^ <*e*> by A18, A19, GLIB_001:83
.= <*e0,e*> by FINSEQ_1:def 9 ;
e0 <> e by A1, A18, GLIB_000:def 13;
then C0 .edgeSeq() is one-to-one by A25, FINSEQ_3:94;
hence C0 is Trail-like by GLIB_001:def 27; :: thesis: verum

end;

for m, n being odd Element of NAT st m < n & n <= len C0 & C0 . m = C0 . n holds
( m = 1 & n = len C0 )

proof

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len C0 & C0 . m = C0 . n implies ( m = 1 & n = len C0 ) )
A26: ( 1 in dom P9 & 3 in dom P9 ) by A17, FINSEQ_3:25;
then A27: C0 . 1 = P0 .first() by A14, GLIB_001:65;
A28: C0 . 3 = P9 . 3 by A14, A26, GLIB_001:65
.= <*(P0 .first()),e0,(P0 .last())*> . 3 by A18, A19, GLIB_001:def 5
.= P0 .last() ;
A29: C0 . 5 = C0 . ((len P9) + 2) by A17
.= P0 .first() by A14, GLIB_001:65 ;
A30: P0 .first() <> P0 .last()

proof

assume P0 .first() = P0 .last() ; :: thesis: contradiction
then Endvertices P = {(P0 .first())} by A11, ENUMSET1:29;
hence contradiction by A2, CARD_1:30; :: thesis: verum

end;

assume A31: ( m < n & n <= len C0 & C0 . m = C0 . n ) ; :: thesis: ( m = 1 & n = len C0 )
then not not n = 0 & ... & not n = 5 by A22;

per cases then ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) ;

suppose n = 0 ; :: thesis: ( m = 1 & n = len C0 )

hence ( m = 1 & n = len C0 ) ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: ( m = 1 & n = len C0 )

hence ( m = 1 & n = len C0 ) by A31, CHORD:2; :: thesis: verum

end;

suppose n = 2 ; :: thesis: ( m = 1 & n = len C0 )

hence ( m = 1 & n = len C0 ) by POLYFORM:5; :: thesis: verum

end;

suppose A33: n = 3 ; :: thesis: ( m = 1 & n = len C0 )

then A34: m <= 3 - 2 by A31, CHORD:3;
1 <= m by CHORD:2;
then m = 1 by A34, XXREAL_0:1;
hence ( m = 1 & n = len C0 ) by A27, A28, A30, A31, A33; :: thesis: verum

end;

suppose n = 4 ; :: thesis: ( m = 1 & n = len C0 )

hence ( m = 1 & n = len C0 ) by POLYFORM:7; :: thesis: verum

end;

suppose A36: n = 5 ; :: thesis: ( m = 1 & n = len C0 )

then A37: m <= 5 - 2 by A31, CHORD:3;
1 <= m by CHORD:2;
then not not m = 1 + 0 & ... & not m = 1 + 2 by A37, NAT_1:62;

per cases then ( m = 1 or m = 2 or m = 3 ) ;

suppose m = 1 ; :: thesis: ( m = 1 & n = len C0 )

hence ( m = 1 & n = len C0 ) by A22, A36; :: thesis: verum

end;

suppose m = 2 ; :: thesis: ( m = 1 & n = len C0 )

hence ( m = 1 & n = len C0 ) by POLYFORM:5; :: thesis: verum

end;

suppose m = 3 ; :: thesis: ( m = 1 & n = len C0 )

hence ( m = 1 & n = len C0 ) by A28, A29, A30, A31, A36; :: thesis: verum

end;

end;

end;

end;

end;

then C0 is Path-like by A24, GLIB_001:def 28;
hence C0 is Cycle-like by A21, A23; :: thesis: verum

end;

end;

end;

hence C is Cycle-like by A9; :: thesis: verum