theorem Th76: :: GLIB_008:76

for G2 being _Graph
for v being object
for V1 being set
for V2 being finite set
for G1 being addAdjVertexAll of G2,v,V1 \/ V2 st V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 & V1 misses V2 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V2) + 2 & p . 2 is addAdjVertexAll of G2,v,V1 & ( for n being Element of dom p st 2 <= n & n <= (len p) - 1 holds
ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) ) )