let W be Walk of T; ( W is Trail-like implies W is Path-like )
assume A1:
W is Trail-like
; W is Path-like
defpred S1[ Nat] means ( T is odd & T <= len W & ex k being odd Element of NAT st
( k < T & W . k = W . T ) );
assume
not W is Path-like
; contradiction
then
ex m, n being odd Element of NAT st
( m < n & n <= len W & W . m = W . n & ( m <> 1 or n <> len W ) )
by A1;
then A2:
ex p being Nat st S1[p]
;
consider p being Nat such that
A3:
S1[p]
and
A4:
for r being Nat st S1[r] holds
p <= r
from NAT_1:sch 5(A2);
reconsider P = p as Element of NAT by ORDINAL1:def 12;
consider k being odd Element of NAT such that
A5:
k < p
and
p <= len W
and
A6:
W . k = W . p
by A3;
set Wc = W .cut (k,P);
(len (W .cut (k,P))) + k = P + 1
by A3, A5, GLIB_001:36;
then
len (W .cut (k,P)) <> 1
by A5;
then A7:
W .cut (k,P) is V5()
by GLIB_001:126;
A8:
(W .cut (k,P)) .last() = W . p
by A3, A5, GLIB_001:37;
A9:
W .cut (k,P) is Path-like
proof
assume
not
W .cut (
k,
P) is
Path-like
;
contradiction
then consider m,
n being
odd Element of
NAT such that A10:
m < n
and A11:
n <= len (W .cut (k,P))
and A12:
(W .cut (k,P)) . m = (W .cut (k,P)) . n
and A13:
(
m <> 1 or
n <> len (W .cut (k,P)) )
by A1;
A14:
m < len (W .cut (k,P))
by A10, A11, XXREAL_0:2;
consider kn1 being
odd Nat such that A15:
(W .cut (k,P)) . n = W . kn1
and A16:
kn1 = (k + n) - 1
and A17:
kn1 <= len W
by A3, A5, A11, Th12;
reconsider kn1 =
kn1 as
odd Element of
NAT by ORDINAL1:def 12;
A18:
1
<= m
by ABIAN:12;
m <= len (W .cut (k,P))
by A10, A11, XXREAL_0:2;
then consider km1 being
odd Nat such that A19:
(W .cut (k,P)) . m = W . km1
and A20:
km1 = (k + m) - 1
and A21:
km1 <= len W
by A3, A5, Th12;
reconsider km1 =
km1 as
odd Element of
NAT by ORDINAL1:def 12;
per cases
( n < len (W .cut (k,P)) or n = len (W .cut (k,P)) )
by A11, XXREAL_0:1;
suppose
n < len (W .cut (k,P))
;
contradictionthen
k + n < k + (len (W .cut (k,P)))
by XREAL_1:6;
then
k + n < p + 1
by A3, A5, GLIB_001:36;
then A22:
kn1 < p
by A16, XREAL_1:19;
k + m < k + n
by A10, XREAL_1:6;
then
km1 < kn1
by A20, A16, XREAL_1:9;
hence
contradiction
by A4, A12, A19, A15, A17, A22;
verum end; suppose A23:
n = len (W .cut (k,P))
;
contradiction
k + m < (len (W .cut (k,P))) + k
by A14, XREAL_1:6;
then
k + m < p + 1
by A3, A5, GLIB_001:36;
then A24:
km1 < p
by A20, XREAL_1:19;
1
< m
by A13, A18, A23, XXREAL_0:1;
then
k + 1
< k + m
by XREAL_1:6;
then
k < km1
by A20, XREAL_1:20;
hence
contradiction
by A4, A6, A8, A12, A19, A21, A23, A24;
verum end; end;
end;
(W .cut (k,P)) .first() = W . k
by A3, A5, GLIB_001:37;
then
W .cut (k,P) is closed
by A6, A8;
then
W .cut (k,P) is Cycle-like
by A7, A9;
hence
contradiction
by GLIB_002:def 2; verum