let G2 be _Graph; :: thesis: for v being object
for V being 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) + 2 & p . 2 is addVertex of G2,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 ) ) ) )
let v be object ; :: thesis: for V being 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) + 2 & p . 2 is addVertex of G2,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 ) ) ) )
let V be finite set ; :: thesis: 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) + 2 & p . 2 is addVertex of G2,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 ) ) ) )
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V) + 2 & p . 2 is addVertex of G2,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 ) ) ) ) )
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis: ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V) + 2 & p . 2 is addVertex of G2,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 ) ) ) )
( V = V \/ {} & {} misses V ) by XBOOLE_1:65;
then consider p being non empty Graph-yielding FinSequence such that
A2: ( p . 1 = G2 & p . (len p) = G1 & len p = (card V) + 2 ) and
A3: p . 2 is addAdjVertexAll of G2,v, {} and
A4: 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 ) ) by A1, Th76;
take p ; :: thesis: ( p . 1 = G2 & p . (len p) = G1 & len p = (card V) + 2 & p . 2 is addVertex of G2,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 ) ) ) )
thus ( p . 1 = G2 & p . (len p) = G1 & len p = (card V) + 2 ) by A2; :: thesis: ( p . 2 is addVertex of G2,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 ) ) ) )
thus p . 2 is addVertex of G2,v by A3, GLIB_007:55; :: thesis: 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 ) )
thus 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 ) ) by A4; :: thesis: verum