let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is Path-like implies G2 is Path-like )
assume A1: ( G1 == G2 & G1 is Path-like ) ; :: thesis: G2 is Path-like
hence G2 is Tree-like by GLIB_002:48; :: according to GLPACY00:def 1 :: thesis: for v being Vertex of G2 holds v .degree() c= 2
let v2 be Vertex of G2; :: thesis: v2 .degree() c= 2
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
v1 .degree() = v2 .degree() by A1, GLIB_000:96;
hence v2 .degree() c= 2 by A1; :: thesis: verum