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 A2, FINSEQ_3:25;

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 A4, JORDAN12:2, XXREAL_0:1;

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 A3, XREAL_1:13;

hence n - 1 in dom W by A5, FINSEQ_3:25; :: thesis: ( n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )

n < len W by A3, XXREAL_0:1;

then n + 1 <= len W by NAT_1:13;

hence n + 1 in dom W by A1, FINSEQ_3:25; :: thesis: W . n Joins W . naa1,W . (n + 1),G

n - 1 < (len W) - 0 by A3, XREAL_1:15;

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

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 A2, FINSEQ_3:25;

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 A4, JORDAN12:2, XXREAL_0:1;

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 A3, XREAL_1:13;

hence n - 1 in dom W by A5, FINSEQ_3:25; :: thesis: ( n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )

n < len W by A3, XXREAL_0:1;

then n + 1 <= len W by NAT_1:13;

hence n + 1 in dom W by A1, FINSEQ_3:25; :: thesis: W . n Joins W . naa1,W . (n + 1),G

n - 1 < (len W) - 0 by A3, XREAL_1:15;

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