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

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 :: thesis: for x being odd Element of NAT st x <= len W holds

( W .find (W . x) = x & W .rfind (W . x) = x )

( W .find (W . x) = x & W .rfind (W . x) = x )

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 .rfind (W . x) >= x by Th113;

A5: W .find (W . x) = W .rfind (W . x) by A1, A3;

W .find (W . x) <= x by A3, Th113;

hence ( W .find (W . x) = x & W .rfind (W . x) = x ) by A4, A5, XXREAL_0:1; :: thesis: verum

end;assume A3: x <= len W ; :: thesis: ( W .find (W . x) = x & W .rfind (W . x) = x )

then A4: W .rfind (W . x) >= x by Th113;

A5: W .find (W . x) = W .rfind (W . x) by A1, A3;

W .find (W . x) <= x by A3, Th113;

hence ( W .find (W . x) = x & W .rfind (W . x) = x ) by A4, A5, XXREAL_0:1; :: thesis: verum

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n

then A20:
W is Trail-like
by Lm57;W . m <> W . n

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

assume that

A6: 1 <= m and

A7: m < n and

A8: n <= len W ; :: thesis: W . m <> W . n

1 <= n by A6, A7, XXREAL_0:2;

then n in dom W by A8, FINSEQ_3:25;

then consider naa1 being odd Element of NAT such that

A9: naa1 = n - 1 and

A10: n - 1 in dom W and

A11: n + 1 in dom W and

A12: W . n Joins W . naa1,W . (n + 1),G by Lm2;

m <= len W by A7, A8, XXREAL_0:2;

then m in dom W by A6, FINSEQ_3:25;

then consider maa1 being odd Element of NAT such that

A13: maa1 = m - 1 and

A14: m - 1 in dom W and

m + 1 in dom W and

A15: W . m Joins W . maa1,W . (m + 1),G by Lm2;

end;assume that

A6: 1 <= m and

A7: m < n and

A8: n <= len W ; :: thesis: W . m <> W . n

1 <= n by A6, A7, XXREAL_0:2;

then n in dom W by A8, FINSEQ_3:25;

then consider naa1 being odd Element of NAT such that

A9: naa1 = n - 1 and

A10: n - 1 in dom W and

A11: n + 1 in dom W and

A12: W . n Joins W . naa1,W . (n + 1),G by Lm2;

m <= len W by A7, A8, XXREAL_0:2;

then m in dom W by A6, FINSEQ_3:25;

then consider maa1 being odd Element of NAT such that

A13: maa1 = m - 1 and

A14: m - 1 in dom W and

m + 1 in dom W and

A15: W . m Joins W . maa1,W . (m + 1),G by Lm2;

now :: thesis: not W . m = W . n

hence
W . m <> W . n
; :: thesis: verumset Wnaa1 = W . naa1;

set Wn1 = W . (n + 1);

set Wmaa1 = W . maa1;

set Wm1 = W . (m + 1);

assume A16: W . m = W . n ; :: thesis: contradiction

maa1 <= len W by A13, A14, FINSEQ_3:25;

then A17: W .find (W . maa1) = maa1 by A2;

A18: n + 1 <= len W by A11, FINSEQ_3:25;

A19: naa1 <= len W by A9, A10, FINSEQ_3:25;

end;set Wn1 = W . (n + 1);

set Wmaa1 = W . maa1;

set Wm1 = W . (m + 1);

assume A16: W . m = W . n ; :: thesis: contradiction

maa1 <= len W by A13, A14, FINSEQ_3:25;

then A17: W .find (W . maa1) = maa1 by A2;

A18: n + 1 <= len W by A11, FINSEQ_3:25;

A19: naa1 <= len W by A9, A10, FINSEQ_3:25;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;

now :: thesis: for m, n being odd Element of NAT st m < n & n <= len W & W . m = W . n holds

( m = 1 & n = len W )

hence
W is Path-like
by A20; :: thesis: verum( m = 1 & n = len W )

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 that

A21: m < n and

A22: n <= len W and

A23: W . m = W . n ; :: thesis: ( m = 1 & n = len W )

m <= len W by A21, A22, XXREAL_0:2;

then W .find (W . m) = m by A2;

hence ( m = 1 & n = len W ) by A2, A21, A22, A23; :: thesis: verum

end;assume that

A21: m < n and

A22: n <= len W and

A23: W . m = W . n ; :: thesis: ( m = 1 & n = len W )

m <= len W by A21, A22, XXREAL_0:2;

then W .find (W . m) = m by A2;

hence ( m = 1 & n = len W ) by A2, A21, A22, A23; :: thesis: verum