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

for n being odd Element of NAT st n <= len W holds

W .vertexAt n in W .vertices()

let W be Walk of G; :: thesis: for n being odd Element of NAT st n <= len W holds

W .vertexAt n in W .vertices()

let n be odd Element of NAT ; :: thesis: ( n <= len W implies W .vertexAt n in W .vertices() )

assume A1: n <= len W ; :: thesis: W .vertexAt n in W .vertices()

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

hence W .vertexAt n in W .vertices() by A1, Lm45; :: thesis: verum

for n being odd Element of NAT st n <= len W holds

W .vertexAt n in W .vertices()

let W be Walk of G; :: thesis: for n being odd Element of NAT st n <= len W holds

W .vertexAt n in W .vertices()

let n be odd Element of NAT ; :: thesis: ( n <= len W implies W .vertexAt n in W .vertices() )

assume A1: n <= len W ; :: thesis: W .vertexAt n in W .vertices()

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

hence W .vertexAt n in W .vertices() by A1, Lm45; :: thesis: verum