let G2 be _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 ) ) ) )
let v be 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 ) ) ) )
let V be 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 ) ) ) )
let G1 be addAdjVertexAll of G2,v,V; ( 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) + 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 ) ) ) ) )
assume A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
; 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 ) ) ) )
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
; ( 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 ) ) ) )
thus
( p . 1 = G2 & p . (len p) = G1 )
by A2; ( 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 ) ) ) )
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
; ( 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 ) ) ) )
hereby 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 ) )
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
proof
defpred S1[
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:
S1[
0 ]
A9:
for
m being
Nat st
S1[
m] holds
S1[
m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A10:
S1[
m]
;
S1[m + 1]
assume A11:
(m + 1) + 2
<= len p
;
ex k being Element of dom p st
( k = (m + 1) + 2 & e in the_Edges_of (p . k) )
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
;
( k = (m + 1) + 2 & e in the_Edges_of (p . k) )
thus
k = (m + 1) + 2
;
e in the_Edges_of (p . k)
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;
verum
end;
A15:
for
m being
Nat holds
S1[
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;
verum
end; take w =
w;
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 ) )take e =
e;
( 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 ) )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;
verum
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; verum