theorem Th60: :: GLIB_008:60

for G being _finite _Graph
for H being Subgraph of G st G .size() = H .size() holds
ex p being non empty Graph-yielding _finite 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) ) ) )