let G be _Graph; :: thesis: for W being Walk of G holds W .vertices() = (W .reverse() ) .vertices()
let W be Walk of G; :: thesis: W .vertices() = (W .reverse() ) .vertices()

now

let x be set ; :: thesis: ( ( x in W .vertices() implies x in (W .reverse() ) .vertices() ) & ( x in (W .reverse() ) .vertices() implies x in W .vertices() ) )

hereby :: thesis: ( x in (W .reverse() ) .vertices() implies x in W .vertices() )

assume x in W .vertices() ; :: thesis: x in (W .reverse() ) .vertices()
then consider n being odd Element of NAT such that
A2: ( n <= len W & W . n = x ) by Lm45;
1 <= n by HEYTING3:1;
then A3: n in dom W by A2, FINSEQ_3:27;
then A4: (W .reverse() ) . (((len W) - n) + 1) = x by A2, Th25;
reconsider lenW = len W as odd Element of NAT ;
A5: (lenW - n) + 1 is odd Element of NAT by A2, FINSEQ_5:1;
n in Seg (len W) by A3, FINSEQ_1:def 3;
then (lenW - n) + 1 in Seg (len W) by FINSEQ_5:2;
then A7: (lenW - n) + 1 in dom W by FINSEQ_1:def 3;
(lenW - n) + 1 <= len W by A7, FINSEQ_3:27;
then A8: (lenW - n) + 1 <= len (W .reverse() ) by FINSEQ_5:def 3;
thus x in (W .reverse() ) .vertices() by A4, A5, A8, Lm45; :: thesis: verum

end;

assume x in (W .reverse() ) .vertices() ; :: thesis: x in W .vertices()
then consider n being odd Element of NAT such that
A10: ( n <= len (W .reverse() ) & (W .reverse() ) . n = x ) by Lm45;
A11: 1 <= n by HEYTING3:1;
then n in dom (W .reverse() ) by A10, FINSEQ_3:27;
then A12: W . (((len W) - n) + 1) = x by A10, FINSEQ_5:def 3;
reconsider lenW = len W as odd Element of NAT ;
A13: n <= len W by A10, FINSEQ_5:def 3;
then A14: (lenW - n) + 1 is odd Element of NAT by FINSEQ_5:1;
n in Seg (len W) by A11, A13, FINSEQ_1:3;
then (lenW - n) + 1 in Seg (len W) by FINSEQ_5:2;
then A15: (lenW - n) + 1 <= len W by FINSEQ_1:3;
thus x in W .vertices() by A12, A14, A15, Lm45; :: thesis: verum

end;

hence W .vertices() = (W .reverse() ) .vertices() by TARSKI:2; :: thesis: verum