let G be _Graph; :: thesis: for W being Walk of G st ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
m = n ) holds
W is Path-like

let W be Walk of G; :: thesis: ( ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
m = n ) implies W is Path-like )

assume A1: for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
m = n ; :: thesis: W is Path-like
now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
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
A2: 1 <= m and
A3: m < n and
A4: n <= len W ; :: thesis: W . m <> W . n
m <= len W by ;
then A5: m in dom W by ;
1 <= n by ;
then A6: n in dom W by ;
now :: thesis: not W . m = W . n
assume W . m = W . n ; :: thesis: contradiction
then consider naa1 being odd Element of NAT such that
A7: naa1 = n - 1 and
A8: n - 1 in dom W and
A9: n + 1 in dom W and
A10: W . m Joins W . naa1,W . (n + 1),G by ;
A11: naa1 <= len W by ;
consider maa1 being odd Element of NAT such that
A12: maa1 = m - 1 and
A13: m - 1 in dom W and
A14: m + 1 in dom W and
A15: W . m Joins W . maa1,W . (m + 1),G by ;
A16: maa1 <= len W by ;
A17: n + 1 <= len W by ;
A18: m + 1 <= len W by ;
now :: thesis: contradiction
per cases ( ( W . naa1 = W . maa1 & W . (n + 1) = W . (m + 1) ) or ( W . naa1 = W . (m + 1) & W . (n + 1) = W . maa1 ) ) by ;
suppose ( W . naa1 = W . maa1 & W . (n + 1) = W . (m + 1) ) ; :: thesis: contradiction
end;
suppose A19: ( W . naa1 = W . (m + 1) & W . (n + 1) = W . maa1 ) ; :: thesis: contradiction
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence W . m <> W . n ; :: thesis: verum
end;
then A21: W is Trail-like by Lm57;
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 )
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
A22: m < n and
A23: n <= len W ; :: thesis: ( W . m = W . n implies ( m = 1 & n = len W ) )
assume A24: W . m = W . n ; :: thesis: ( m = 1 & n = len W )
m <= len W by ;
hence ( m = 1 & n = len W ) by A1, A22, A23, A24; :: thesis: verum
end;
hence W is Path-like by A21; :: thesis: verum