let P be non _trivial Path-like _Graph; :: thesis: for v being Vertex of P st not v is endvertex holds
v .degree() = 2
let v be Vertex of P; :: thesis: ( not v is endvertex implies v .degree() = 2 )
assume not v is endvertex ; :: thesis: v .degree() = 2
then A1: v .degree() <> 1 by GLIB_000:174;
v .degree() <> 0 by GLIB_000:157;
then not v .degree() in {0,1} by A1, TARSKI:def 2;
then A2: 2 c= v .degree() by CARD_1:50, ORDINAL1:16;
v .degree() c= 2 by Def1;
hence v .degree() = 2 by A2, XBOOLE_0:def 10; :: thesis: verum