let G be locally-finite _Graph; :: thesis: ( G is Path-like iff ( G is Tree-like & ( for v being Vertex of G holds v .degree() <= 2 ) ) )

hereby :: thesis: ( G is Tree-like & ( for v being Vertex of G holds v .degree() <= 2 ) implies G is Path-like )

assume A1: G is Path-like ; :: thesis: ( G is Tree-like & ( for v being Vertex of G holds v .degree() <= 2 ) )
hence G is Tree-like ; :: thesis: for v being Vertex of G holds v .degree() <= 2
let v be Vertex of G; :: thesis: v .degree() <= 2
Segm (v .degree()) c= Segm 2 by A1;
hence v .degree() <= 2 by NAT_1:39; :: thesis: verum

end;

assume A2: G is Tree-like ; :: thesis: ( ex v being Vertex of G st not v .degree() <= 2 or G is Path-like )
assume A3: for v being Vertex of G holds v .degree() <= 2 ; :: thesis: G is Path-like
thus G is Tree-like by A2; :: according to GLPACY00:def 1 :: thesis: for v being Vertex of G holds v .degree() c= 2
let v be Vertex of G; :: thesis: v .degree() c= 2
Segm (v .degree()) c= Segm 2 by A3, NAT_1:39;
hence v .degree() c= 2 ; :: thesis: verum