theorem :: GLPACY00:18

for p being non empty Graph-yielding FinSequence st not p . 1 is _trivial & 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 & ( v1 in Endvertices (p . n) or v2 in Endvertices (p . n) ) ) ) holds
p . (len p) is Path-like