let C be Cycle-like _Graph; :: thesis: for e being Edge of C
for P being removeEdge of C,e holds
( P is _finite & P is Path-like )
let e be Edge of C; :: thesis: for P being removeEdge of C,e holds
( P is _finite & P is Path-like )
let P be removeEdge of C,e; :: thesis: ( P is _finite & P is Path-like )
thus P is _finite ; :: thesis: P is Path-like
A1: the_Edges_of P = (the_Edges_of C) \ {e} by GLIB_000:51;

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_Edges_of C = W9 .edges() by Th39
.= W .edges() by GLIB_001:110 ;
then e in W .edges() ;
hence contradiction by A1, ZFMISC_1:56; :: thesis: verum

end;

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

now :: thesis: ex W being Walk of C st
( W is Cycle-like & e in W .edges() )

consider W being Walk of C such that
A4: W is Cycle-like by GLIB_002:def 2;
take W = W; :: thesis: ( W is Cycle-like & e in W .edges() )
the_Edges_of C = W .edges() by A4, Th39;
hence ( W is Cycle-like & e in W .edges() ) by A4; :: thesis: verum

end;

then P is connected by GLIB_002:5;
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 v be Vertex of P; :: thesis: v .degree() c= 2
reconsider w = v as Vertex of C by GLIB_000:def 33;
v .degree() <= w .degree() by GLIB_000:81;
then v .degree() <= 2 by GLIB_016:def 4;
hence v .degree() c= 2 by FIELD_5:3; :: thesis: verum