set VE = (the_Vertices_of G) \/ (the_Edges_of G);
set W = <*v*>;
set v9 = v;
reconsider v9 = v as Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;
<*v9*> is FinSequence of (the_Vertices_of G) \/ (the_Edges_of G)
;
then reconsider W = <*v*> as FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) ;
now ( len W is odd & W . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len <*v*> holds
W . (n + 1) Joins W . n,W . (n + 2),G ) )thus
len W is
odd
by FINSEQ_1:40, JORDAN12:2;
( W . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len <*v*> holds
W . (n + 1) Joins W . n,W . (n + 2),G ) )
W . 1
= v
by FINSEQ_1:40;
hence
W . 1
in the_Vertices_of G
;
for n being odd Element of NAT st n < len <*v*> holds
W . (n + 1) Joins W . n,W . (n + 2),Glet n be
odd Element of
NAT ;
( n < len <*v*> implies W . (n + 1) Joins W . n,W . (n + 2),G )A1:
1
<= n
by ABIAN:12;
assume
n < len <*v*>
;
W . (n + 1) Joins W . n,W . (n + 2),Ghence
W . (n + 1) Joins W . n,
W . (n + 2),
G
by A1, FINSEQ_1:40;
verum end;
hence
<*v*> is Walk of G
by Def3; verum