let G be _Graph; :: thesis: for W being Walk of G

for n being odd Element of NAT st 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 n < len W holds

W . (n + 1) in (W .vertexAt n) .edgesInOut()

let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) in (W .vertexAt n) .edgesInOut() )

assume A1: n < len W ; :: thesis: W . (n + 1) in (W .vertexAt n) .edgesInOut()

then A2: W .vertexAt n = W . n by Def8;

W . (n + 1) Joins W . n,W . (n + 2),G by A1, Def3;

hence W . (n + 1) in (W .vertexAt n) .edgesInOut() by A2, GLIB_000:62; :: thesis: verum

for n being odd Element of NAT st 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 n < len W holds

W . (n + 1) in (W .vertexAt n) .edgesInOut()

let n be odd Element of NAT ; :: thesis: ( n < len W implies W . (n + 1) in (W .vertexAt n) .edgesInOut() )

assume A1: n < len W ; :: thesis: W . (n + 1) in (W .vertexAt n) .edgesInOut()

then A2: W .vertexAt n = W . n by Def8;

W . (n + 1) Joins W . n,W . (n + 2),G by A1, Def3;

hence W . (n + 1) in (W .vertexAt n) .edgesInOut() by A2, GLIB_000:62; :: thesis: verum