theorem Th68: :: GLIB_008:68

for G being _finite _Graph
for H being Subgraph of G ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = (((G .order()) + (G .size())) - ((H .order()) + (H .size()))) + 1 & ( for n being Element of dom p holds
( not n <= (len p) - 1 or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) or ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) ) )