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

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

let W be Walk of G; :: thesis: ( W is Trail-like implies W .reverse() is Trail-like )
assume A2: W is Trail-like ; :: thesis: W .reverse() is Trail-like

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

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

end;

hence W .reverse() is Trail-like by Lm57; :: thesis: verum

end;

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