set VE = () \/ ();
set W = <*v*>;
set v9 = v;
reconsider v9 = v as Element of () \/ () by XBOOLE_0:def 3;
<*v9*> is FinSequence of () \/ () ;
then reconsider W = <*v*> as FinSequence of () \/ () ;
now :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: for n being odd Element of NAT st n < len <*v*> holds
W . (n + 1) Joins W . n,W . (n + 2),G

let n be odd Element of NAT ; :: thesis: ( n < len <*v*> implies W . (n + 1) Joins W . n,W . (n + 2),G )
A1: 1 <= n by ABIAN:12;
assume n < len <*v*> ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G
hence W . (n + 1) Joins W . n,W . (n + 2),G by ; :: thesis: verum
end;
hence <*v*> is Walk of G by Def3; :: thesis: verum