set W9 = Rev W;
reconsider W9 = Rev W as FinSequence of () \/ () ;
A1: len W9 = len W by FINSEQ_5:def 3;
now :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: for n being odd Element of NAT st n < len W9 holds
W9 . (n + 1) Joins W9 . n,W9 . (n + 2),G

let n be odd Element of NAT ; :: thesis: ( 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 ; :: thesis: W9 . (n + 1) Joins W9 . n,W9 . (n + 2),G
then A3: n + 1 <= len W by ;
then reconsider rnaa1 = ((len W) - (n + 1)) + 1 as even Element of NAT by FINSEQ_5:1;
n + 1 < len W by ;
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 ;
then A5: W9 . (n + 1) = W . rnaa1 by FINSEQ_5:58
.= W . (rn2 + 1) ;
A6: n <= len W by ;
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 ;
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 ;
then W9 . (n + 1) Joins W9 . (n + 2),W9 . n,G by ;
hence W9 . (n + 1) Joins W9 . n,W9 . (n + 2),G by GLIB_000:14; :: thesis: verum
end;
hence Rev W is Walk of G by Def3; :: thesis: verum