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:
A3: now :: thesis: for m, n being odd Element of NAT st m < n & n <= len () & () . m = () . n holds
( m = 1 & n = len () )
let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len () & () . m = () . n implies ( m = 1 & n = len () ) )
assume that
A4: m < n and
A5: n <= len () and
A6: (W .reverse()) . m = () . n ; :: thesis: ( m = 1 & n = len () )
A7: 1 <= m by ABIAN:12;
m <= len () by ;
then A8: m in dom () by ;
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 () by ;
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 ;
then A11: rn < rm by XREAL_1:8;
(W .reverse()) . n = W . (((len W) - n) + 1) by ;
then A12: W . rm = W . rn by A6, A8, Lm8;
A13: rm <= len W by ;
then (len W) + (1 + (- m)) = len W by A2, A11, A12;
hence m = 1 ; :: thesis: n = len ()
rn = 1 by A2, A11, A13, A12;
hence n = len () 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