theorem Th61: :: GLIB_008:61

for G being _finite edgeless _Graph
for H being Subgraph of G ex p being non empty Graph-yielding _finite edgeless FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )