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 ( not T is even & 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, GLIB_001:def 28;
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 13;
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:37;
then len (W .cut k,P) <> 1 by A5;
then A7: not W .cut k,P is trivial by GLIB_001:127;
A8: (W .cut k,P) .last() = W . p by A3, A5, GLIB_001:38;
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, GLIB_001:def 28;
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 13;
A18: 1 <= m by HEYTING3:1;
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 13;

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:8;
then k + n < p + 1 by A3, A5, GLIB_001:37;
then A22: kn1 < p by A16, XREAL_1:21;
k + m < k + n by A10, XREAL_1:8;
then km1 < kn1 by A20, A16, XREAL_1:11;
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:8;
then k + m < p + 1 by A3, A5, GLIB_001:37;
then A24: km1 < p by A20, XREAL_1:21;
1 < m by A13, A18, A23, XXREAL_0:1;
then k + 1 < k + m by XREAL_1:8;
then k < km1 by A20, XREAL_1:22;
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:38;
then W .cut k,P is closed by A6, A8, GLIB_001:def 24;
then W .cut k,P is Cycle-like by A7, A9, GLIB_001:def 31;
hence contradiction by GLIB_002:def 2; :: thesis: verum