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