let G be _Graph; :: thesis: for W being Walk of G holds
( W is Path-like iff W .reverse() is Path-like )
let W be Walk of G; :: thesis: ( W is Path-like iff W .reverse() is Path-like )

A1: now :: thesis: for W being Walk of G st W is Path-like holds
W .reverse() is Path-like

let W be Walk of G; :: thesis: ( W is Path-like implies W .reverse() is Path-like )
reconsider lenW = len W as odd Element of NAT ;
assume A2: W is Path-like ; :: thesis: W .reverse() is Path-like

A3: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len (W .reverse()) & (W .reverse()) . m = (W .reverse()) . n holds
( m = 1 & n = len (W .reverse()) )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len (W .reverse()) & (W .reverse()) . m = (W .reverse()) . n implies ( m = 1 & n = len (W .reverse()) ) )
assume that
A4: m < n and
A5: n <= len (W .reverse()) and
A6: (W .reverse()) . m = (W .reverse()) . n ; :: thesis: ( m = 1 & n = len (W .reverse()) )
A7: 1 <= m by ABIAN:12;
m <= len (W .reverse()) by A4, A5, XXREAL_0:2;
then A8: m in dom (W .reverse()) by A7, FINSEQ_3:25;
then A9: ((len W) - m) + 1 in dom W by Lm8;
then reconsider rm = (lenW - m) + 1 as odd Element of NAT ;
1 <= n by ABIAN:12;
then A10: n in dom (W .reverse()) by A5, FINSEQ_3:25;
then ((len W) - n) + 1 in dom W by Lm8;
then reconsider rn = (lenW - n) + 1 as odd Element of NAT ;
lenW - n < (len W) - m by A4, XREAL_1:15;
then A11: rn < rm by XREAL_1:8;
(W .reverse()) . n = W . (((len W) - n) + 1) by A10, Lm8;
then A12: W . rm = W . rn by A6, A8, Lm8;
A13: rm <= len W by A9, FINSEQ_3:25;
then (len W) + (1 + (- m)) = len W by A2, A11, A12;
hence m = 1 ; :: thesis: n = len (W .reverse())
rn = 1 by A2, A11, A13, A12;
hence n = len (W .reverse()) by FINSEQ_5:def 3; :: thesis: verum

end;

W is Trail-like by A2;
then W .reverse() is Trail-like by Lm58;
hence W .reverse() is Path-like by A3; :: thesis: verum

end;

hence ( W is Path-like implies W .reverse() is Path-like ) ; :: thesis: ( W .reverse() is Path-like implies W is Path-like )
assume W .reverse() is Path-like ; :: thesis: W is Path-like
then (W .reverse()) .reverse() is Path-like by A1;
hence W is Path-like ; :: thesis: verum