let G1 be non _trivial _Graph; for W being Walk of G1
for v being Vertex of G1
for G2 being removeVertex of G1,v st not v in W .vertices() holds
W is Walk of G2
let W be Walk of G1; for v being Vertex of G1
for G2 being removeVertex of G1,v st not v in W .vertices() holds
W is Walk of G2
let v be Vertex of G1; for G2 being removeVertex of G1,v st not v in W .vertices() holds
W is Walk of G2
let G2 be removeVertex of G1,v; ( not v in W .vertices() implies W is Walk of G2 )
assume A1:
not v in W .vertices()
; W is Walk of G2
set EG2 = (the_Edges_of G1) \ (v .edgesInOut());
set W2 = W;
set VG2 = (the_Vertices_of G1) \ {v};
v .edgesInOut() = G1 .edgesInOut {v}
by GLIB_000:def 40;
then A2:
(the_Edges_of G1) \ (v .edgesInOut()) = G1 .edgesBetween ((the_Vertices_of G1) \ {v})
by GLIB_000:35;
then
rng W c= (the_Vertices_of G2) \/ (the_Edges_of G2)
by TARSKI:def 3;
then reconsider W2 = W as FinSequence of (the_Vertices_of G2) \/ (the_Edges_of G2) by FINSEQ_1:def 4;
now ( len W2 is odd & W2 . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W2 holds
W . (n + 1) Joins W . n,W . (n + 2),G2 ) )reconsider lenW2 =
len W2 as
odd Element of
NAT ;
thus
len W2 is
odd
;
( W2 . 1 in the_Vertices_of G2 & ( for n being odd Element of NAT st n < len W2 holds
W . (n + 1) Joins W . n,W . (n + 2),G2 ) )
W .first() in W .vertices()
by Th86;
then A16:
not
W2 . 1
in {v}
by A1, TARSKI:def 1;
W .first() in the_Vertices_of G1
;
then
W2 . 1
in (the_Vertices_of G1) \ {v}
by A16, XBOOLE_0:def 5;
hence
W2 . 1
in the_Vertices_of G2
by GLIB_000:47;
for n being odd Element of NAT st n < len W2 holds
W . (n + 1) Joins W . n,W . (n + 2),G2let n be
odd Element of
NAT ;
( n < len W2 implies W . (n + 1) Joins W . n,W . (n + 2),G2 )assume A17:
n < len W2
;
W . (n + 1) Joins W . n,W . (n + 2),G2then A18:
W . (n + 1) Joins W . n,
W . (n + 2),
G1
by Def3;
then A19:
W . (n + 1) in the_Edges_of G1
by GLIB_000:def 13;
n + 1
<= len W2
by A17, NAT_1:13;
then
n + 1
< lenW2
by XXREAL_0:1;
then
(n + 1) + 1
<= len W2
by NAT_1:13;
then A20:
W . (n + 2) <> v
by A1, Lm45;
W . n <> v
by A1, A17, Lm45;
then
not
W . (n + 1) in v .edgesInOut()
by A18, A20, GLIB_000:65;
then
W . (n + 1) in (the_Edges_of G1) \ (v .edgesInOut())
by A19, XBOOLE_0:def 5;
then
W . (n + 1) in the_Edges_of G2
by A2, GLIB_000:47;
hence
W . (n + 1) Joins W . n,
W . (n + 2),
G2
by A18, GLIB_000:73;
verum end;
hence
W is Walk of G2
by Def3; verum