theorem Th79: :: GLIB_008:79

for G being _finite simple _Graph
for W being set
for H being inducedSubgraph of G,W ex p being non empty Graph-yielding _finite simple 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 object ex V being finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) )