let G be _Graph; 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; ( ( 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
; 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 A2:
1
<= m
and A3:
m < n
and A4:
n <= len W
;
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 not W . m = W . nassume
W . m = W . n
;
contradictionthen 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;
hence
contradiction
;
verum end; hence
W . m <> W . n
;
verum end;
then A21:
W is Trail-like
by Lm57;
hence
W is Path-like
by A21; verum