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
assume not W is Path-like ; :: thesis: contradiction
then consider m, n being odd Element of NAT such that
A2: m < n and
A3: n <= len W and
A4: W . m = W . n and
( m <> 1 or n <> len W ) by A1, GLIB_001:def 28;
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 ) );
A5: ex p being Nat st S₁[p] by A2, A3, A4;
consider p being Nat such that
A6: S₁[p] and
A7: for r being Nat st S₁[r] holds
p <= r from NAT_1:sch 5(A5);
reconsider P = p as Element of NAT by ORDINAL1:def 13;
consider k being odd Element of NAT such that
A8: k < p and
p <= len W and
A9: W . k = W . p by A6;
set Wc = W .cut k,P;
(len (W .cut k,P)) + k = P + 1 by A6, A8, GLIB_001:37;
then len (W .cut k,P) <> 1 by A8;
then A10: not W .cut k,P is trivial by GLIB_001:127;
A11: W .cut k,P is Trail-like by A1;
A12: (W .cut k,P) .first() = W . k by A6, A8, GLIB_001:38;
A13: (W .cut k,P) .last() = W . p by A6, A8, GLIB_001:38;
A14: 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
A15: m < n and
A16: n <= len (W .cut k,P) and
A17: (W .cut k,P) . m = (W .cut k,P) . n and
A18: ( m <> 1 or n <> len (W .cut k,P) ) by A11, GLIB_001:def 28;
A19: 1 <= m by HEYTING3:1;
A20: m <= len (W .cut k,P) by A15, A16, XXREAL_0:2;
A21: m < len (W .cut k,P) by A15, A16, XXREAL_0:2;
consider km1 being odd Nat such that
A22: (W .cut k,P) . m = W . km1 and
A23: km1 = (k + m) - 1 and
A24: km1 <= len W by A6, A8, A20, Th12;
reconsider km1 = km1 as odd Element of NAT by ORDINAL1:def 13;
consider kn1 being odd Nat such that
A25: (W .cut k,P) . n = W . kn1 and
A26: kn1 = (k + n) - 1 and
A27: kn1 <= len W by A6, A8, A16, Th12;
reconsider kn1 = kn1 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 A16, 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 A6, A8, GLIB_001:37;
then A28: kn1 < p by A26, XREAL_1:21;
k + m < k + n by A15, XREAL_1:8;
then km1 < kn1 by A23, A26, XREAL_1:11;
hence contradiction by A7, A17, A22, A25, A27, A28; :: thesis: verum

end;

suppose A29: n = len (W .cut k,P) ; :: thesis: contradiction

then 1 < m by A18, A19, XXREAL_0:1;
then k + 1 < k + m by XREAL_1:8;
then A30: k < km1 by A23, XREAL_1:22;
k + m < (len (W .cut k,P)) + k by A21, XREAL_1:8;
then k + m < p + 1 by A6, A8, GLIB_001:37;
then km1 < p by A23, XREAL_1:21;
hence contradiction by A7, A9, A13, A17, A22, A24, A29, A30; :: thesis: verum

end;

end;

end;

W .cut k,P is closed by A9, A12, A13, GLIB_001:def 24;
then W .cut k,P is Cycle-like by A10, A14, GLIB_001:def 31;
hence contradiction by GLIB_002:def 2; :: thesis: verum