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

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

hence
W is vertex-distinct
; :: thesis: verumm = 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;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