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 ) )
assume 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 A1: ( 1 <= n & n <= len W ) by FINSEQ_3:27;
then reconsider naa1 = n - 1 as odd Element of NAT by INT_1:18;
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 A1, JORDAN12:3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then (1 + 1) - 1 <= n - 1 by XREAL_1:15;
then A2: 1 <= naa1 ;
n - 1 <= (len W) - 0 by A1, XREAL_1:15;
hence n - 1 in dom W by A2, FINSEQ_3:27; :: thesis: ( n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )
n < len W by A1, XXREAL_0:1;
then A3: n + 1 <= len W by NAT_1:13;
1 <= 1 + n by NAT_1:12;
hence n + 1 in dom W by A3, FINSEQ_3:27; :: thesis: W . n Joins W . naa1,W . (n + 1),G
n - 1 < (len W) - 0 by A1, XREAL_1:17;
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