set VE = (the_Vertices_of G) \/ (the_Edges_of G);

hereby :: thesis: ( not e Joins x,y,G implies G .walkOf the Element of the_Vertices_of G is Walk of G )

thus
( not e Joins x,y,G implies G .walkOf the Element of the_Vertices_of G is Walk of G )
; :: thesis: verumset W = <*x,e,y*>;

assume A1: e Joins x,y,G ; :: thesis: <*x,e,y*> is Walk of G

then y is Vertex of G by GLIB_000:13;

then A2: y is Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

e in the_Edges_of G by A1, GLIB_000:def 13;

then A3: e is Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

x is Vertex of G by A1, GLIB_000:13;

then x is Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

then reconsider W = <*x,e,y*> as FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) by A2, A3, FINSEQ_2:14;

A4: W . 1 = x by FINSEQ_1:45;

A5: W . 2 = e by FINSEQ_1:45;

end;assume A1: e Joins x,y,G ; :: thesis: <*x,e,y*> is Walk of G

then y is Vertex of G by GLIB_000:13;

then A2: y is Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

e in the_Edges_of G by A1, GLIB_000:def 13;

then A3: e is Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

x is Vertex of G by A1, GLIB_000:13;

then x is Element of (the_Vertices_of G) \/ (the_Edges_of G) by XBOOLE_0:def 3;

then reconsider W = <*x,e,y*> as FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) by A2, A3, FINSEQ_2:14;

A4: W . 1 = x by FINSEQ_1:45;

A5: W . 2 = e by FINSEQ_1:45;

now :: thesis: ( len W is odd & W . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len W holds

W . (n + 1) Joins W . n,W . (n + 2),G ) )

hence
<*x,e,y*> is Walk of G
by Def3; :: thesis: verumW . (n + 1) Joins W . n,W . (n + 2),G ) )

reconsider aa1 = 1 as odd Element of NAT by JORDAN12:2;

aa1 + 2 is odd ;

hence len W is odd by FINSEQ_1:45; :: thesis: ( W . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len W holds

W . (n + 1) Joins W . n,W . (n + 2),G ) )

thus W . 1 in the_Vertices_of G by A1, A4, GLIB_000:13; :: thesis: for n being odd Element of NAT st n < len W holds

W . (n + 1) Joins W . n,W . (n + 2),G

let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G )

assume n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G

then n < 2 + 1 by FINSEQ_1:45;

then n <= 2 by NAT_1:13;

then not not n = 0 & ... & not n = 2 ;

hence W . (n + 1) Joins W . n,W . (n + 2),G by A1, A4, A5, FINSEQ_1:45; :: thesis: verum

end;aa1 + 2 is odd ;

hence len W is odd by FINSEQ_1:45; :: thesis: ( W . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len W holds

W . (n + 1) Joins W . n,W . (n + 2),G ) )

thus W . 1 in the_Vertices_of G by A1, A4, GLIB_000:13; :: thesis: for n being odd Element of NAT st n < len W holds

W . (n + 1) Joins W . n,W . (n + 2),G

let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G )

assume n < len W ; :: thesis: W . (n + 1) Joins W . n,W . (n + 2),G

then n < 2 + 1 by FINSEQ_1:45;

then n <= 2 by NAT_1:13;

then not not n = 0 & ... & not n = 2 ;

hence W . (n + 1) Joins W . n,W . (n + 2),G by A1, A4, A5, FINSEQ_1:45; :: thesis: verum