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