let C be non _trivial Cycle-like _Graph; :: thesis: for v being Vertex of C
for P being removeVertex of C,v holds
( P is _finite & P is Path-like )
let v be Vertex of C; :: thesis: for P being removeVertex of C,v holds
( P is _finite & P is Path-like )
let P be removeVertex of C,v; :: thesis: ( P is _finite & P is Path-like )
thus P is _finite ; :: thesis: P is Path-like
A1: the_Vertices_of P = (the_Vertices_of C) \ {v} by GLIB_000:47;

now :: thesis: for W being Walk of P holds not W is Cycle-like

given W being Walk of P such that A2: W is Cycle-like ; :: thesis: contradiction
reconsider W9 = W as Walk of C by GLIB_001:167;
W9 is Cycle-like by A2, GLIB_006:24;
then the_Vertices_of C = W9 .vertices() by Th39
.= W .vertices() by GLIB_001:98 ;
then v in W .vertices() ;
hence contradiction by A1, ZFMISC_1:56; :: thesis: verum

end;

then A3: P is acyclic by GLIB_002:def 2;

now :: thesis: for u, w being Vertex of P ex W being Walk of P st W is_Walk_from u,w

let u, w be Vertex of P; :: thesis: ex W being Walk of P st W is_Walk_from u,w
consider C9 being Walk of C such that
A4: C9 is Cycle-like by GLIB_002:def 2;
the_Vertices_of P c= the_Vertices_of C ;
then the_Vertices_of P c= C9 .vertices() by A4, Th39;
then A5: ( u in C9 .vertices() & w in C9 .vertices() ) by TARSKI:def 3;
v in {v} by TARSKI:def 1;
then ( u <> v & w <> v ) by A1, XBOOLE_0:def 5;
then consider W being Path of C such that
A6: ( W is_Walk_from u,w & not v in W .vertices() ) by A4, A5, Th5;
reconsider W = W as Walk of P by A6, GLIB_001:171;
take W = W; :: thesis: W is_Walk_from u,w
thus W is_Walk_from u,w by A6, GLIB_001:19; :: thesis: verum

end;

then P is connected by GLIB_002:def 1;
hence P is Tree-like by A3; :: according to GLPACY00:def 1 :: thesis: for v being Vertex of P holds v .degree() c= 2
let u be Vertex of P; :: thesis: u .degree() c= 2
reconsider w = u as Vertex of C by A1, XBOOLE_0:def 5;
u .degree() <= w .degree() by GLIB_000:81;
then u .degree() <= 2 by GLIB_016:def 4;
hence u .degree() c= 2 by FIELD_5:3; :: thesis: verum