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 A3, A4, XXREAL_0:2;
then A5: m in dom W by A2, FINSEQ_3:25;
1 <= n by A2, A3, XXREAL_0:2;
then A6: n in dom W by A4, FINSEQ_3:25;
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 A6, Lm2;
A11: naa1 <= len W by A7, A8, FINSEQ_3:25;
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 A5, Lm2;
A16: maa1 <= len W by A12, A13, FINSEQ_3:25;
A17: n + 1 <= len W by A9, FINSEQ_3:25;
A18: m + 1 <= len W by A14, FINSEQ_3:25;
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 A15, A10, GLIB_000:15;
suppose ( W . naa1 = W . maa1 & W . (n + 1) = W . (m + 1) ) ; :: thesis: contradiction
then naa1 = maa1 by A1, A16, A11;
hence contradiction by A3, A12, A7; :: thesis: verum
end;
suppose A19: ( W . naa1 = W . (m + 1) & W . (n + 1) = W . maa1 ) ; :: thesis: contradiction
then A20: n + 1 = maa1 by A1, A16, A17;
naa1 = m + 1 by A1, A18, A11, A19;
hence contradiction by A12, A7, A20; :: thesis: verum
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 A22, A23, XXREAL_0:2;
hence ( m = 1 & n = len W ) by A1, A22, A23, A24; :: thesis: verum
end;
hence W is Path-like by A21; :: thesis: verum