let P be _finite non _trivial Path-like _Graph; :: thesis: 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 )
let v be object ; :: thesis: 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 )
let C be addAdjVertexAll of P,v, Endvertices P; :: thesis: ( not v in the_Vertices_of P implies ( C is simple & C is Cycle-like ) )
assume A1: not v in the_Vertices_of P ; :: thesis: ( C is simple & C is Cycle-like )
thus C is simple ; :: thesis: C is Cycle-like
card (Endvertices P) <> 0 by Th37;
then Endvertices P <> {} ;
hence C is connected ; :: according to GLPACY00:def 6 :: thesis: ( not C is acyclic & C is 2 -regular )
consider w1, w2 being Vertex of P such that
A2: ( w1 <> w2 & Endvertices P = {w1,w2} ) by Th36;
ex G3 being Component of P ex w1, w2 being Vertex of G3 st
( w1 in Endvertices P & w2 in Endvertices P & w1 <> w2 )

proof

reconsider G3 = P as Component of P by GLIB_002:30;
reconsider w1 = w1, w2 = w2 as Vertex of G3 ;
take G3 ; :: thesis: ex w1, w2 being Vertex of G3 st
( w1 in Endvertices P & w2 in Endvertices P & w1 <> w2 )
take w1 ; :: thesis: ex w2 being Vertex of G3 st
( w1 in Endvertices P & w2 in Endvertices P & w1 <> w2 )
take w2 ; :: thesis: ( w1 in Endvertices P & w2 in Endvertices P & w1 <> w2 )
thus ( w1 in Endvertices P & w2 in Endvertices P & w1 <> w2 ) by A2, TARSKI:def 2; :: thesis: verum

end;

hence not C is acyclic by A1, GLIB_007:71; :: thesis: C is 2 -regular

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

let u be Vertex of C; :: thesis: b₁ .degree() = 2
A3: ( w1 in Endvertices P & w2 in Endvertices P ) by A2, TARSKI:def 2;

per cases ( u = w1 or u = w2 or u = v or ( u <> w1 & u <> w2 & u <> v ) ) ;

suppose u = w1 ; :: thesis: b₁ .degree() = 2

hence u .degree() = (w1 .degree()) +` 1 by A1, A3, GLIBPRE0:57
.= 1 +` 1 by A3, GLIB_000:def 52, GLIB_006:56
.= 2 ;
:: thesis: verum

end;

suppose u = w2 ; :: thesis: b₁ .degree() = 2

hence u .degree() = (w2 .degree()) +` 1 by A1, A3, GLIBPRE0:57
.= 1 +` 1 by A3, GLIB_000:def 52, GLIB_006:56
.= 2 ;
:: thesis: verum

end;

suppose u = v ; :: thesis: b₁ .degree() = 2

hence u .degree() = card (Endvertices P) by A1, GLIBPRE0:55
.= 2 by A2, CARD_2:57 ;
:: thesis: verum

end;

suppose A4: ( u <> w1 & u <> w2 & u <> v ) ; :: thesis: b₁ .degree() = 2

then A5: not u in Endvertices P by A2, TARSKI:def 2;
A6: the_Vertices_of C = (the_Vertices_of P) \/ {v} by A1, GLIB_007:def 4;
not u in {v} by A4, TARSKI:def 1;
then reconsider u9 = u as Vertex of P by A6, XBOOLE_0:def 3;
A7: not u9 is endvertex by A5, GLIB_006:56;
thus u .degree() = u9 .degree() by A5, GLIBPRE0:56
.= 2 by A7, Th35 ; :: thesis: verum

end;

end;

end;

hence C is 2 -regular by GLIB_016:def 4; :: thesis: verum