let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be non empty finite set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
assume A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) ; :: thesis:
set v0 = the Element of V;
set V0 = V \ { the Element of V};
the Element of V in { the Element of V} by TARSKI:def 1;
then not the Element of V in V \ { the Element of V} by XBOOLE_0:def 5;
then ( V = (V \ { the Element of V}) \/ { the Element of V} & { the Element of V} misses V \ { the Element of V} ) by ZFMISC_1:50, ZFMISC_1:116;
then consider p being non empty Graph-yielding FinSequence such that
A2: ( p . 1 = G2 & p . (len p) = G1 & len p = (card (V \ { the Element of V})) + 2 ) and
A3: p . 2 is addAdjVertexAll of G2,v,{ the Element of 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:
thus ( p . 1 = G2 & p . (len p) = G1 ) by A2; :: thesis:
thus len p = ((card V) - (card { the Element of V})) + 2 by A2, CARD_2:44
.= ((card V) - 1) + 2 by CARD_1:30
.= (card V) + 1 ; :: thesis:

reconsider w = the Element of V as Vertex of G2 by A1, TARSKI:def 3;
consider e being object such that
A5: not e in the_Edges_of G2 and
A6: ( p . 2 is addAdjVertex of G2,v,e,w or p . 2 is addAdjVertex of G2,w,e,v ) by A1, A3, GLIB_007:56;
A7: e in the_Edges_of G1

defpred S₁[ Nat] means ( $1 + 2 <= len p implies ex k being Element of dom p st
( k = $1 + 2 & e in the_Edges_of (p . k) ) );
A8: S₁[ 0 ]

assume 0 + 2 <= len p ; :: thesis:
((card (V \ { the Element of V})) + 2) - (card (V \ { the Element of V})) <= (len p) - 0 by A2, XREAL_1:10;
then reconsider k = 2 as Element of dom p by FINSEQ_3:25;
take k ; :: thesis:
thus k = 0 + 2 ; :: thesis:

end;

end;

A9: for m being Nat st S₁[m] holds
S₁[m + 1]

let m be Nat; :: thesis:
assume A10: S₁[m] ; :: thesis:
assume A11: (m + 1) + 2 <= len p ; :: thesis:
then ((m + 1) + 2) - 1 <= (len p) - 0 by XREAL_1:13;
then consider k0 being Element of dom p such that
A12: ( k0 = m + 2 & e in the_Edges_of (p . k0) ) by A10;
1 + 0 <= (m + 1) + 2 by XREAL_1:7;
then reconsider k = (m + 1) + 2 as Element of dom p by A11, FINSEQ_3:25;
take k ; :: thesis:
thus k = (m + 1) + 2 ; :: thesis:
A13: 0 + (1 + 1) <= m + (1 + 1) by XREAL_1:7;
((m + 1) + 2) - 1 <= (len p) - 1 by A11, XREAL_1:9;
then consider u being Vertex of G2, f being object such that
f in (the_Edges_of G1) \ (the_Edges_of (p . k0)) and
A14: ( p . (k0 + 1) is addEdge of p . k0,v,f,u or p . (k0 + 1) is addEdge of p . k0,u,f,v ) by A4, A12, A13;
the_Edges_of (p . k0) c= the_Edges_of (p . k) by A12, A14, GLIB_006:def 9;
hence e in the_Edges_of (p . k) by A12; :: thesis:

end;

A15: for m being Nat holds S₁[m] from NAT_1:sch 2(A8, A9);
reconsider m = (len p) - 2 as Nat by A2;
consider k being Element of dom p such that
A16: ( k = m + 2 & e in the_Edges_of (p . k) ) by A15;
thus e in the_Edges_of G1 by A2, A16; :: thesis:

end;

take w = w; :: thesis:
take e = e; :: thesis:
thus ( 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 ) ) by A5, A6, A7, XBOOLE_0:def 5; :: thesis:

end;

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: