let G be _Graph; :: thesis: for W being Walk of G
for n being even Element of NAT st n in dom W holds
ex naa1 being odd Element of NAT st
( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )

let W be Walk of G; :: thesis: for n being even Element of NAT st n in dom W holds
ex naa1 being odd Element of NAT st
( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )

let n be even Element of NAT ; :: thesis: ( n in dom W implies ex naa1 being odd Element of NAT st
( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G ) )

A1: 1 <= 1 + n by NAT_1:12;
assume A2: n in dom W ; :: thesis: ex naa1 being odd Element of NAT st
( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )

then A3: n <= len W by FINSEQ_3:25;
A4: 1 <= n by ;
then reconsider naa1 = n - 1 as odd Element of NAT by INT_1:5;
take naa1 ; :: thesis: ( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )
thus naa1 = n - 1 ; :: thesis: ( n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )
1 < n by ;
then 1 + 1 <= n by NAT_1:13;
then (1 + 1) - 1 <= n - 1 by XREAL_1:13;
then A5: 1 <= naa1 ;
n - 1 <= (len W) - 0 by ;
hence n - 1 in dom W by ; :: thesis: ( n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )
n < len W by ;
then n + 1 <= len W by NAT_1:13;
hence n + 1 in dom W by ; :: thesis: W . n Joins W . naa1,W . (n + 1),G
n - 1 < (len W) - 0 by ;
then W . (naa1 + 1) Joins W . naa1,W . (naa1 + 2),G by Def3;
hence W . n Joins W . naa1,W . (n + 1),G ; :: thesis: verum