set VE = (the_Vertices_of G) \/ (the_Edges_of G);
hereby ( not e Joins x,y,G implies G .walkOf the Element of the_Vertices_of G is Walk of G )
set W =
<*x,e,y*>;
assume A1:
e Joins x,
y,
G
;
<*x,e,y*> is Walk of Gthen
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 ( 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 ) )reconsider aa1 = 1 as
odd Element of
NAT by JORDAN12:2;
aa1 + 2 is
odd
;
hence
len W is
odd
by FINSEQ_1:45;
( 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;
for n being odd Element of NAT st n < len W holds
W . (n + 1) Joins W . n,W . (n + 2),Glet n be
odd Element of
NAT ;
( n < len W implies W . (n + 1) Joins W . n,W . (n + 2),G )assume
n < len W
;
W . (n + 1) Joins W . n,W . (n + 2),Gthen
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;
verum end; hence
<*x,e,y*> is
Walk of
G
by Def3;
verum
end;
thus
( not e Joins x,y,G implies G .walkOf the Element of the_Vertices_of G is Walk of G )
; verum