theorem :: GLIB_008:83

for p being non empty Graph-yielding FinSequence st p . 1 is simple & p . 1 is connected & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty set st p . (n + 1) is addAdjVertexAll of p . n,v,V ) holds
( p . (len p) is simple & p . (len p) is connected )