let H be Subgraph of P; :: thesis: ( H is connected implies H is Path-like )
assume H is connected ; :: thesis: H is Path-like
hence H is Tree-like ; :: according to GLPACY00:def 1 :: thesis: for v being Vertex of H holds v .degree() c= 2
let v2 be Vertex of H; :: thesis: v2 .degree() c= 2
the_Vertices_of H c= the_Vertices_of P ;
then reconsider v1 = v2 as Vertex of P by TARSKI:def 3;
A2: v2 .degree() c= v1 .degree() by Th1;
v1 .degree() c= 2 by Def1;
hence v2 .degree() c= 2 by A2, XBOOLE_1:1; :: thesis: verum