let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism & G2 is Path-like holds
G1 is Path-like
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism & G2 is Path-like implies G1 is Path-like )
assume A1: ( F is isomorphism & G2 is Path-like ) ; :: thesis: G1 is Path-like
then ( G1 is connected & G1 is acyclic ) by GLIB_010:140;
hence G1 is Tree-like ; :: according to GLPACY00:def 1 :: thesis: for v being Vertex of G1 holds v .degree() c= 2
let v be Vertex of G1; :: thesis: v .degree() c= 2
((F _V) /. v) .degree() c= 2 by A1;
hence v .degree() c= 2 by A1, GLIBPRE0:93; :: thesis: verum