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 .find (W . n) = W .rfind (W . 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 .find (W . n) = W .rfind (W . n) ) implies W is Path-like )
assume A1: for n being odd Element of NAT st n <= len W holds
W .find (W . n) = W .rfind (W . n) ; :: thesis: W is Path-like

A2: now

let x be odd Element of NAT ; :: thesis: ( x <= len W implies ( W .find (W . x) = x & W .rfind (W . x) = x ) )
assume A3: x <= len W ; :: thesis: ( W .find (W . x) = x & W .rfind (W . x) = x )
then A4: W .find (W . x) <= x by Th116;
A5: W .rfind (W . x) >= x by A3, Th116;
W .find (W . x) = W .rfind (W . x) by A1, A3;
hence ( W .find (W . x) = x & W .rfind (W . x) = x ) by A4, A5, XXREAL_0:1; :: thesis: verum

end;

now

let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len W implies W . m <> W . n )
assume A6: ( 1 <= m & m < n & n <= len W ) ; :: thesis: W . m <> W . n
then ( 1 <= m & m <= len W ) by XXREAL_0:2;
then m in dom W by FINSEQ_3:27;
then consider maa1 being odd Element of NAT such that
A7: ( maa1 = m - 1 & m - 1 in dom W & m + 1 in dom W & W . m Joins W . maa1,W . (m + 1),G ) by Lm2;
( 1 <= n & n <= len W ) by A6, XXREAL_0:2;
then n in dom W by FINSEQ_3:27;
then consider naa1 being odd Element of NAT such that
A8: ( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G ) by Lm2;

now

assume A9: W . m = W . n ; :: thesis: contradiction
set Wmaa1 = W . maa1;
set Wm1 = W . (m + 1);
set Wnaa1 = W . naa1;
set Wn1 = W . (n + 1);
A10: ( maa1 <= len W & n + 1 <= len W & naa1 <= len W ) by A7, A8, FINSEQ_3:27;
then A11: ( W .find (W . maa1) = maa1 & W .rfind (W . naa1) = naa1 & W .rfind (W . (n + 1)) = n + 1 ) by A2;

now

per cases ( ( W . maa1 = W . naa1 & W . (m + 1) = W . (n + 1) ) or ( W . maa1 = W . (n + 1) & W . (m + 1) = W . naa1 ) ) by A7, A8, A9, GLIB_000:18;

suppose ( W . maa1 = W . naa1 & W . (m + 1) = W . (n + 1) ) ; :: thesis: contradiction

then maa1 = naa1 by A1, A10, A11;
hence contradiction by A6, A7, A8; :: thesis: verum

end;

suppose ( W . maa1 = W . (n + 1) & W . (m + 1) = W . naa1 ) ; :: thesis: contradiction

then maa1 = n + 1 by A1, A10, A11;
then n <= (maa1 - 1) + 1 by NAT_1:12;
then n <= (m - 1) + 1 by A7, NAT_1:12;
hence contradiction by A6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence W . m <> W . n ; :: thesis: verum

end;

then A12: W is Trail-like by Lm57;

now

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W & W . m = W . n implies ( m = 1 & n = len W ) )
assume A13: ( m < n & n <= len W & W . m = W . n ) ; :: thesis: ( m = 1 & n = len W )
then m <= len W by XXREAL_0:2;
then ( W .find (W . m) = m & W .find (W . m) = n ) by A2, A13;
hence ( m = 1 & n = len W ) by A13; :: thesis: verum

end;

hence W is Path-like by A12, Def28; :: thesis: verum