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