theorem Th67: :: GLIB_008:67

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