let G be _Graph; :: thesis: for W being Walk of G
for n being odd Element of NAT st 1 < n & n <= len W holds
W . (n - 1) in (W .vertexAt n) .edgesInOut()
let W be Walk of G; :: thesis: for n being odd Element of NAT st 1 < n & n <= len W holds
W . (n - 1) in (W .vertexAt n) .edgesInOut()
let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len W implies W . (n - 1) in (W .vertexAt n) .edgesInOut() )
assume that
A1: 1 < n and
A2: n <= len W ; :: thesis: W . (n - 1) in (W .vertexAt n) .edgesInOut()
reconsider naa1 = n - 1 as even Element of NAT by A1, INT_1:5;
1 + 1 <= n by A1, NAT_1:13;
then A3: (1 + 1) - 1 <= n - 1 by XREAL_1:13;
n - 1 <= (len W) - 0 by A2, XREAL_1:13;
then naa1 in dom W by A3, FINSEQ_3:25;
then consider n5 being odd Element of NAT such that
A4: n5 = naa1 - 1 and
A5: naa1 - 1 in dom W and
naa1 + 1 in dom W and
A6: W . naa1 Joins W . n5,W . (naa1 + 1),G by Lm2;
n5 <= len W by A4, A5, FINSEQ_3:25;
then W . n5 = W .vertexAt n5 by Def8;
then W . (n - 1) Joins W .vertexAt n5,W .vertexAt n,G by A2, A6, Def8;
hence W . (n - 1) in (W .vertexAt n) .edgesInOut() by GLIB_000:14, GLIB_000:62; :: thesis: verum