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 A1: ( 1 < n & n <= len W ) ; :: thesis: W . (n - 1) in (W .vertexAt n) .edgesInOut()
then reconsider naa1 = n - 1 as even Element of NAT by INT_1:18;
A2: n - 1 <= (len W) - 0 by A1, XREAL_1:15;
1 + 1 <= n by A1, NAT_1:13;
then (1 + 1) - 1 <= n - 1 by XREAL_1:15;
then naa1 in dom W by A2, FINSEQ_3:27;
then consider n5 being odd Element of NAT such that
A3: ( n5 = naa1 - 1 & naa1 - 1 in dom W & naa1 + 1 in dom W & W . naa1 Joins W . n5,W . (naa1 + 1),G ) by Lm2;
n5 <= len W by A3, FINSEQ_3:27;
then W . n5 = W .vertexAt n5 by Def8;
then W . (n - 1) Joins W .vertexAt n5,W .vertexAt n,G by A1, A3, Def8;
hence W . (n - 1) in (W .vertexAt n) .edgesInOut() by GLIB_000:17, GLIB_000:65; :: thesis: verum