let P be _Graph; :: thesis: ( P is Path-like implies ( P is Tree-like & P is locally-finite & P is with_max_degree ) )
assume A1: P is Path-like ; :: thesis: ( P is Tree-like & P is locally-finite & P is with_max_degree )
hence P is Tree-like ; :: thesis: ( P is locally-finite & P is with_max_degree )

now :: thesis: for v being Vertex of P holds v .degree() is finite

let v be Vertex of P; :: thesis: v .degree() is finite
v .degree() c= 2 by A1;
hence v .degree() is finite ; :: thesis: verum

end;

hence P is locally-finite by GLIB_013:23; :: thesis: P is with_max_degree
thus P is with_max_degree by A1, Th13; :: thesis: verum