theorem
for
G2 being
_Graph for
v being
object for
V being non
empty finite set for
G1 being
addAdjVertexAll of
G2,
v,
V st
V c= the_Vertices_of G2 & not
v in the_Vertices_of G2 holds
ex
p being non
empty Graph-yielding FinSequence st
(
p . 1
= G2 &
p . (len p) = G1 &
len p = (card V) + 1 & ex
w being
Vertex of
G2 ex
e being
object st
(
e in (the_Edges_of G1) \ (the_Edges_of G2) & (
p . 2 is
addAdjVertex of
G2,
v,
e,
w or
p . 2 is
addAdjVertex of
G2,
w,
e,
v ) ) & ( 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 ) ) ) )