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 in the_Vertices_of G

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

W . n in the_Vertices_of G

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

assume n <= len W ; :: thesis: W . n in the_Vertices_of G

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

hence W . n in the_Vertices_of G ; :: thesis: verum

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

W . n in the_Vertices_of G

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

W . n in the_Vertices_of G

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

assume n <= len W ; :: thesis: W . n in the_Vertices_of G

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

hence W . n in the_Vertices_of G ; :: thesis: verum