theorem :: GLIB_008:70

for p being non empty Graph-yielding FinSequence st p . 1 is finite & ( for n being Element of dom p holds
( not n <= (len p) - 1 or ex v being object st p . (n + 1) is addVertex of p . n,v or ex v1, e, v2 being object st p . (n + 1) is addEdge of p . n,v1,e,v2 ) ) holds
p . (len p) is finite