theorem Th148: :: GLIB_001:150

for G being _Graph
for W being Path of G
for e, v being object st e Joins W .last() ,v,G & not e in W .edges() & ( not W is trivial or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) holds
W .addEdge e is Path-like