theorem :: GLPACY00:16

for p being non empty Graph-yielding FinSequence st p . 1 is Path-like & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & ( p . n is _trivial or v1 in Endvertices (p . n) or v2 in Endvertices (p . n) ) ) ) holds
p . (len p) is Path-like