set VE = (the_Vertices_of G) \/ (the_Edges_of G);
consider v being object such that
A1: v in the_Vertices_of G by XBOOLE_0:def 1;
reconsider v = v as Element of (the_Vertices_of G) \/ (the_Edges_of G) by A1, XBOOLE_0:def 3;
take <*v*> ; :: thesis: ( len <*v*> is odd & <*v*> . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len <*v*> holds
<*v*> . (n + 1) Joins <*v*> . n,<*v*> . (n + 2),G ) )
thus len <*v*> is odd by FINSEQ_1:40, JORDAN12:2; :: thesis: ( <*v*> . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len <*v*> holds
<*v*> . (n + 1) Joins <*v*> . n,<*v*> . (n + 2),G ) )
thus <*v*> . 1 in the_Vertices_of G by A1; :: thesis: for n being odd Element of NAT st n < len <*v*> holds
<*v*> . (n + 1) Joins <*v*> . n,<*v*> . (n + 2),G
let n be odd Element of NAT ; :: thesis: ( n < len <*v*> implies <*v*> . (n + 1) Joins <*v*> . n,<*v*> . (n + 2),G )
assume n < len <*v*> ; :: thesis: <*v*> . (n + 1) Joins <*v*> . n,<*v*> . (n + 2),G
then n < 1 by FINSEQ_1:40;
hence <*v*> . (n + 1) Joins <*v*> . n,<*v*> . (n + 2),G by ABIAN:12; :: thesis: verum