theorem :: GLIB_008:73

for p being non empty Graph-yielding FinSequence st p . 1 is Tree-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 ) holds
p . (len p) is Tree-like