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