let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )
let v be object ; for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )
let V be set ; for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )
let G1 be addAdjVertexAll of G2,v,V; for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )
let W be Walk of G1; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 implies ( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) ) )
assume A1:
( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 )
; ( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )
consider E being set such that
A2:
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E )
and
A3:
for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) )
by A1, Def4;
A4:
E /\ (the_Edges_of G2) = {}
by A2, XBOOLE_0:def 7;
hereby ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 )
assume A5:
(
W .edges() c= the_Edges_of G2 &
W is
V5() )
;
not v in W .vertices() thus
not
v in W .vertices()
verumproof
assume
v in W .vertices()
;
contradiction
then consider n being
odd Element of
NAT such that A6:
(
n <= len W &
W . n = v )
by GLIB_001:87;
per cases
( n = len W or n < len W )
by A6, XXREAL_0:1;
suppose A7:
n = len W
;
contradictionA8:
1
<> len W
by A5, GLIB_001:126;
1
<= len W
by ABIAN:12;
then
1
< len W
by A8, XXREAL_0:1;
then reconsider m =
(len W) - 2 as
odd Element of
NAT by Lm13;
A9:
m < (len W) - 0
by XREAL_1:15;
then
W . (m + 1) Joins W . m,
W . (m + 2),
G1
by GLIB_001:def 3;
then A10:
W . (m + 1) Joins W . m,
v,
G1
by A6, A7;
then
W . m in V
by A1, Def4;
then consider e1 being
object such that A11:
(
e1 in E &
e1 Joins W . m,
v,
G1 )
and A12:
for
e2 being
object st
e2 Joins W . m,
v,
G1 holds
e1 = e2
by A3;
W . (m + 1) in E
by A10, A11, A12;
then
not
W . (m + 1) in W .edges()
by A5, A4, Lm7;
hence
contradiction
by A9, GLIB_001:100;
verum end; suppose A13:
n < len W
;
contradictionthen A14:
W . (n + 1) Joins W . (n + 2),
v,
G1
by A6, GLIB_000:14, GLIB_001:def 3;
then
W . (n + 2) in V
by A1, Def4;
then consider e1 being
object such that A15:
(
e1 in E &
e1 Joins W . (n + 2),
v,
G1 )
and A16:
for
e2 being
object st
e2 Joins W . (n + 2),
v,
G1 holds
e1 = e2
by A3;
W . (n + 1) in E
by A14, A15, A16;
then
not
W . (n + 1) in W .edges()
by A5, A4, Lm7;
hence
contradiction
by A13, GLIB_001:100;
verum end; end;
end;
end;
assume A17:
not v in W .vertices()
; W .edges() c= the_Edges_of G2
for e being object st e in W .edges() holds
e in the_Edges_of G2
hence
W .edges() c= the_Edges_of G2
by TARSKI:def 3; verum