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 :: 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
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;
hence W is Path-like by Lm66; :: thesis: verum