let W be Walk of G; :: thesis: ( W is trivial implies W is vertex-distinct )
assume A7: W is trivial ; :: thesis: W is vertex-distinct

now :: thesis: for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
m = n

let m, n be odd Element of NAT ; :: thesis: ( m <= len W & n <= len W & W . m = W . n implies m = n )
assume that
A8: m <= len W and
A9: n <= len W and
W . m = W . n ; :: thesis: m = n
A10: 1 <= m by ABIAN:12;
m <= 1 by A7, A8, Lm55;
then A11: m = 1 by A10, XXREAL_0:1;
A12: 1 <= n by ABIAN:12;
n <= 1 by A7, A9, Lm55;
hence m = n by A12, A11, XXREAL_0:1; :: thesis: verum

end;

hence W is vertex-distinct ; :: thesis: verum