let G be _Graph; :: thesis: for W being Walk of G st W is open & W is Path-like holds

W is vertex-distinct

let W be Walk of G; :: thesis: ( W is open & W is Path-like implies W is vertex-distinct )

assume that

A1: W is open and

A2: W is Path-like ; :: thesis: W is vertex-distinct

W is vertex-distinct

let W be Walk of G; :: thesis: ( W is open & W is Path-like implies W is vertex-distinct )

assume that

A1: W is open and

A2: W is Path-like ; :: 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

not m <> n

hence
W is vertex-distinct
; :: thesis: verumnot m <> n

let m, n be odd Element of NAT ; :: thesis: ( m <= len W & n <= len W & W . m = W . n implies not m <> n )

assume that

A3: m <= len W and

A4: n <= len W and

A5: W . m = W . n ; :: thesis: not m <> n

assume A6: m <> n ; :: thesis: contradiction

end;assume that

A3: m <= len W and

A4: n <= len W and

A5: W . m = W . n ; :: thesis: not m <> n

assume A6: m <> n ; :: thesis: contradiction