let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is vertex-distinct holds
W2 is vertex-distinct
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is vertex-distinct holds
W2 is vertex-distinct
let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is vertex-distinct implies W2 is vertex-distinct )
assume A1: W1 = W2 ; :: thesis: ( not W1 is vertex-distinct or W2 is vertex-distinct )
assume W1 is vertex-distinct ; :: thesis: W2 is vertex-distinct
then for m, n being odd Element of NAT st m <= len W2 & n <= len W2 & W2 . m = W2 . n holds
m = n by A1, GLIB_001:def 29;
hence W2 is vertex-distinct by GLIB_001:def 29; :: thesis: verum