let P be non _trivial Path-like _Graph; :: thesis:

hereby :: thesis:

assume P .order() = 2 ; :: thesis:
then A1: P is 2 -vertex by GLIB_013:def 3;

now :: thesis:

set v = the Vertex of P;
take v = the Vertex of P; :: thesis:
thus A2: v .degree() = 1 by A1, GLIB_000:174; :: thesis:
let w be Vertex of P; :: thesis:
thus w .degree() c= v .degree() by A1, A2, GLIB_000:174; :: thesis:

end;

hence P .maxDegree() = 1 by GLIB_013:48; :: thesis:

end;

assume A3: P .order() <> 2 ; :: thesis:

per cases ;

suppose A4: for v being Vertex of P holds not v is endvertex ; :: thesis:

now :: thesis:

take v = the Vertex of P; :: thesis:
A5: 2 c= v .degree()

proof

assume not 2 c= v .degree() ; :: thesis:
then v .degree() in {0,1} by ORDINAL1:16, CARD_1:50;
then ( v .degree() = 0 or v .degree() = 1 ) by TARSKI:def 2;
hence contradiction by A4, GLIB_000:157, GLIB_000:174; :: thesis:

end;

v .degree() c= 2 by Def1;
hence A6: v .degree() = 2 by A5, XBOOLE_0:def 10; :: thesis:
let w be Vertex of P; :: thesis:
thus w .degree() c= v .degree() by A6, Def1; :: thesis:

end;

hence P .maxDegree() = 2 by GLIB_013:48; :: thesis:

end;

suppose ex v being Vertex of P st v is endvertex ; :: thesis:

then consider v being Vertex of P such that
A7: v is endvertex ;
3 c= P .order()

proof

assume not 3 c= P .order() ; :: thesis:
then P .order() in {0,1,2} by ORDINAL1:16, CARD_1:51;
then ( P .order() = 0 or P .order() = 1 ) by A3, ENUMSET1:def 1;
hence contradiction by GLIB_000:26; :: thesis:

end;

then consider u, w being Vertex of P such that
A8: ( u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent ) by A7, GLIBPRE0:95;
consider e being object such that
A9: e Joins u,v,P by A8, CHORD:def 3;
consider W being Walk of P such that
A10: W is_Walk_from u,w by GLIB_002:def 1;
set T = the Trail of W;
the Trail of W is_Walk_from u,w by A10, GLIB_001:160;
then A11: ( the Trail of W .first() = u & the Trail of W .last() = w ) by GLIB_001:def 23;
then A12: 3 <= len the Trail of W by A8, GLIB_001:127, GLIB_001:125;
1 < len the Trail of W by A12, XXREAL_0:2;
then the Trail of W . (1 + 1) Joins the Trail of W . 1, the Trail of W . (1 + 2),P by POLYFORM:4, GLIB_001:def 3;
then A13: the Trail of W . 2 Joins u, the Trail of W . 3,P by A11;
A14: the Trail of W . 3 <> v

proof

assume the Trail of W . 3 = v ; :: thesis:
then v in the Trail of W .vertices() by A12, GLIB_001:87, POLYFORM:6;
hence contradiction by A7, A8, A11, GLIB_001:143; :: thesis:

end;

A16: e <> the Trail of W . 2

proof

assume e = the Trail of W . 2 ; :: thesis:

per cases by A9, A13, GLIB_000:15;

suppose ( u = u & v = the Trail of W . 3 ) ; :: thesis:

hence contradiction by A14; :: thesis:

end;

suppose ( u = the Trail of W . 3 & u = v ) ; :: thesis:

hence contradiction by A14; :: thesis:

end;

end;

end;

now :: thesis:

take u = u; :: thesis:
( the Trail of W . 2 in u .edgesInOut() & e in u .edgesInOut() ) by A9, A13, GLIB_000:62;
then card {( the Trail of W . 2),e} c= card (u .edgesInOut()) by CARD_1:11, ZFMISC_1:32;
then 2 c= card (u .edgesInOut()) by A16, CARD_2:57;
then A17: 2 c= u .degree() by GLIB_000:19;
u .degree() c= 2 by Def1;
hence u .degree() = 2 by A17, XBOOLE_0:def 10; :: thesis:
let x be Vertex of P; :: thesis:
x .degree() c= 2 by Def1;
hence x .degree() c= u .degree() by A17, XBOOLE_1:1; :: thesis:

end;

hence P .maxDegree() = 2 by GLIB_013:48; :: thesis:

end;

end;