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 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 ; :: 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 S1[p] ;
consider p being Nat such that
A3: S1[p] and
A4: for r being Nat st S1[r] holds
p <= r from 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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
then A22: kn1 < p by ;
k + m < k + n by ;
then km1 < kn1 by ;
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 ;
then k + m < p + 1 by ;
then A24: km1 < p by ;
1 < m by ;
then k + 1 < k + m by XREAL_1:6;
then k < km1 by ;
hence contradiction by A4, A6, A8, A12, A19, A21, A23, A24; :: thesis: verum
end;
end;
end;
(W .cut (k,P)) .first() = W . k by ;
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