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

now

let m, n be odd Element of NAT ; :: thesis: ( m <= len W & n <= len W & W . m = W . n implies m = n )
assume A2: ( m <= len W & n <= len W & W . m = W . n ) ; :: thesis: m = n
then A3: ( W .rfind m = m & W .rfind n = n ) by A1;
then A4: n <= m by A2, Def22;
m <= n by A2, A3, Def22;
hence m = n by A4, XXREAL_0:1; :: thesis: verum

end;

hence W is Path-like by Lm66; :: thesis: verum