let G be _Graph; :: thesis: for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds

W .rfind n = n ) holds

W is Path-like

let W be Walk of G; :: thesis: ( ( for n being odd Element of NAT st n <= len W holds

W .rfind n = n ) implies W is Path-like )

assume A1: for n being odd Element of NAT st n <= len W holds

W .rfind n = n ; :: thesis: W is Path-like

W .rfind n = n ) holds

W is Path-like

let W be Walk of G; :: thesis: ( ( for n being odd Element of NAT st n <= len W holds

W .rfind n = n ) implies W is Path-like )

assume A1: for n being odd Element of NAT st n <= len W holds

W .rfind n = n ; :: thesis: W is Path-like

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 Path-like
by Lm66; :: 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

A2: m <= len W and

A3: n <= len W and

A4: W . m = W . n ; :: thesis: m = n

W .rfind n = n by A1, A3;

then A5: m <= n by A2, A3, A4, Def22;

W .rfind m = m by A1, A2;

then n <= m by A2, A3, A4, Def22;

hence m = n by A5, XXREAL_0:1; :: thesis: verum

end;assume that

A2: m <= len W and

A3: n <= len W and

A4: W . m = W . n ; :: thesis: m = n

W .rfind n = n by A1, A3;

then A5: m <= n by A2, A3, A4, Def22;

W .rfind m = m by A1, A2;

then n <= m by A2, A3, A4, Def22;

hence m = n by A5, XXREAL_0:1; :: thesis: verum