theorem :: GLIB_008:63

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