let P2 be Path-like _Graph; :: thesis:
let v2 be Vertex of P2; :: thesis:
let e, w2 be object ; :: thesis:
let P1 be addAdjVertex of P2,v2,e,w2; :: thesis:

per cases ;

suppose A1: ( not e in the_Edges_of P2 & not w2 in the_Vertices_of P2 ) ; :: thesis:

assume A2: ( v2 is endvertex or P2 is _trivial ) ; :: thesis:
thus P1 is Tree-like ; :: according to GLPACY00:def 1 :: thesis:

per cases by A2;

suppose A3: v2 is endvertex ; :: thesis:

reconsider v1 = v2 as Vertex of P1 by GLIB_006:68;
reconsider w1 = w2 as Vertex of P1 by A1, GLIB_006:129;
let v be Vertex of P1; :: thesis:

per cases ;

suppose v = v1 ; :: thesis:

then v .degree() = (v2 .degree()) +` 1 by A1, Th10
.= 1 +` 1 by A3, GLIB_000:174
.= 2 ;
hence v .degree() c= 2 ; :: thesis:

end;

suppose v = w1 ; :: thesis:

then v .degree() = 1 by A1, GLIB_006:141, GLIB_000:174;
then v .degree() in 2 by CARD_1:50, TARSKI:def 2;
hence v .degree() c= 2 by ORDINAL1:def 2; :: thesis:

end;

suppose A4: ( v <> v1 & v <> w1 ) ; :: thesis:

then A5: not v in {w2} by TARSKI:def 1;
the_Vertices_of P1 = (the_Vertices_of P2) \/ {w2} by A1, GLIB_006:def 12;
then reconsider v9 = v as Vertex of P2 by A5, XBOOLE_0:def 3;
v .degree() = v9 .degree() by A4, Th9;
hence v .degree() c= 2 by Def1; :: thesis:

end;

end;

end;

suppose A6: P2 is _trivial ; :: thesis:

let v be Vertex of P1; :: thesis:
A7: P1 .order() = (P2 .order()) +` 1 by A1, GLIB_006:150
.= 1 +` 1 by A6, GLIB_000:26
.= 2 ;
then A8: P1 is vertex-finite ;
not P1 is _trivial by A7, GLIB_000:26;
then A9: v .degree() = 1 by A7, A8, GLIB_008:27, GLIB_000:174;
1 c= succ 1 by XBOOLE_1:7;
hence v .degree() c= 2 by A9; :: thesis:

end;

end;

end;

suppose ( e in the_Edges_of P2 or w2 in the_Vertices_of P2 ) ; :: thesis:

then P1 == P2 by GLIB_006:def 12;
hence ( ( v2 is endvertex or P2 is _trivial ) implies P1 is Path-like ) by Lm3; :: thesis:

end;

end;