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;

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 :: 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 ) )

hence
Rev W is Walk of G
by Def3; :: thesis: verumW9 . (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 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; :: thesis: verum

end;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 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; :: thesis: verum