let W be Walk of T; :: thesis: ( W is Trail-like implies W is Path-like )
assume A1: W is Trail-like ; :: thesis: W is Path-like
defpred S₁[ 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 ; :: thesis: 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 S₁[p] ;
consider p being Nat such that
A3: S₁[p] and
A4: for r being Nat st S₁[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 trivial 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 ; :: thesis: 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)) ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose A23: n = len (W .cut (k,P)) ; :: thesis: 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; :: thesis: 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; :: thesis: verum