set W9 = Rev W;
reconsider W9 = Rev W as FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) ;
A1:
len W9 = len W
by FINSEQ_5:def 3;
now ( len W9 is odd & W9 . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len W9 holds
W9 . (n + 1) Joins W9 . n,W9 . (n + 2),G ) )thus
len W9 is
odd
by A1;
( W9 . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len W9 holds
W9 . (n + 1) Joins W9 . n,W9 . (n + 2),G ) )
W9 . 1
= W .last()
by FINSEQ_5:62;
hence
W9 . 1
in the_Vertices_of G
;
for n being odd Element of NAT st n < len W9 holds
W9 . (n + 1) Joins W9 . n,W9 . (n + 2),Glet n be
odd Element of
NAT ;
( n < len W9 implies W9 . (n + 1) Joins W9 . n,W9 . (n + 2),G )set rn =
((len W) - n) + 1;
set rnaa1 =
((len W) - (n + 1)) + 1;
set rn2 =
((len W) - (n + 2)) + 1;
assume A2:
n < len W9
;
W9 . (n + 1) Joins W9 . n,W9 . (n + 2),Gthen A3:
n + 1
<= len W
by A1, NAT_1:13;
then reconsider rnaa1 =
((len W) - (n + 1)) + 1 as
even Element of
NAT by FINSEQ_5:1;
n + 1
< len W
by A3, XXREAL_0:1;
then A4:
(n + 1) + 1
<= len W
by NAT_1:13;
then reconsider rn2 =
((len W) - (n + 2)) + 1 as
odd Element of
NAT by FINSEQ_5:1;
1
<= n + 1
by NAT_1:12;
then
n + 1
in dom W
by A3, FINSEQ_3:25;
then A5:
W9 . (n + 1) =
W . rnaa1
by FINSEQ_5:58
.=
W . (rn2 + 1)
;
A6:
n <= len W
by A2, FINSEQ_5:def 3;
then reconsider rn =
((len W) - n) + 1 as
odd Element of
NAT by FINSEQ_5:1;
1
<= n
by ABIAN:12;
then
n in dom W
by A6, FINSEQ_3:25;
then A7:
W9 . n =
W . rn
by FINSEQ_5:58
.=
W . (rn2 + 2)
;
1
+ 0 < n + 2
by XREAL_1:8;
then
(len W) - (n + 2) < (len W) - 1
by XREAL_1:15;
then
((len W) - (n + 2)) + 1
< ((len W) - 1) + 1
by XREAL_1:8;
then A8:
W . (rn2 + 1) Joins W . rn2,
W . (rn2 + 2),
G
by Def3;
1
<= n + 2
by NAT_1:12;
then
n + 2
in dom W
by A4, FINSEQ_3:25;
then
W9 . (n + 1) Joins W9 . (n + 2),
W9 . n,
G
by A8, A7, A5, FINSEQ_5:58;
hence
W9 . (n + 1) Joins W9 . n,
W9 . (n + 2),
G
by GLIB_000:14;
verum end;
hence
Rev W is Walk of G
by Def3; verum