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 )

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

( 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

hence
( W is Path-like implies W .reverse() is Path-like )
; :: thesis: ( W .reverse() is Path-like implies W is Path-like )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

then W .reverse() is Trail-like by Lm58;

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

end;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()) )

W is Trail-like
by A2;( 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;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

then W .reverse() is Trail-like by Lm58;

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

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