theorem Th22: :: GLPACY00:14

for G being _finite Path-like _Graph
for H being connected Subgraph of G ex p being non empty Graph-yielding _finite Path-like 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 v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (p . n) ) ) ) ) ) )