:: deftheorem Def29 defines vertex-distinct GLIB_001:def 29 :
for G being _Graph
for W being Walk of G holds
( W is vertex-distinct iff for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
m = n );