let G be _Graph; 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; ( ( 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)
; W is Path-like
now for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . nlet m,
n be
even Element of
NAT ;
( 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
;
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;
hence
W . m <> W . n
;
verum end;
then A20:
W is Trail-like
by Lm57;
hence
W is Path-like
by A20; verum