let G2 be _Graph; :: thesis: for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st G1 is Path-like holds
G2 is Path-like
let v1, e, v2 be object ; :: thesis: for G1 being addAdjVertex of G2,v1,e,v2 st G1 is Path-like holds
G2 is Path-like
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis: ( G1 is Path-like implies G2 is Path-like )
assume A1: G1 is Path-like ; :: thesis: G2 is Path-like
then A2: G2 is connected ;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is Path-like by A1, A2; :: thesis: verum