theorem :: GLIB_001:151

for G being _Graph
for W being Path of G
for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() & ( not W is trivial or W is open ) holds
W .addEdge e is Path-like by Lm68;