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

let W be Walk of G; :: thesis: W .vertices() = (W .reverse()) .vertices()

now :: thesis: for x being object holds

( ( x in W .vertices() implies x in (W .reverse()) .vertices() ) & ( x in (W .reverse()) .vertices() implies x in W .vertices() ) )

hence
W .vertices() = (W .reverse()) .vertices()
by TARSKI:2; :: thesis: verum( ( x in W .vertices() implies x in (W .reverse()) .vertices() ) & ( x in (W .reverse()) .vertices() implies x in W .vertices() ) )

reconsider lenW = len W as odd Element of NAT ;

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

then consider n being odd Element of NAT such that

A6: n <= len (W .reverse()) and

A7: (W .reverse()) . n = x by Lm45;

A8: 1 <= n by ABIAN:12;

then n in dom (W .reverse()) by A6, FINSEQ_3:25;

then A9: W . (((len W) - n) + 1) = x by A7, FINSEQ_5:def 3;

A10: n <= len W by A6, FINSEQ_5:def 3;

then n in Seg (len W) by A8, FINSEQ_1:1;

then (lenW - n) + 1 in Seg (len W) by FINSEQ_5:2;

then A11: (lenW - n) + 1 <= len W by FINSEQ_1:1;

(lenW - n) + 1 is odd Element of NAT by A10, FINSEQ_5:1;

hence x in W .vertices() by A9, A11, Lm45; :: thesis: verum

end;let x be object ; :: 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 .reverse()) .vertices()
; :: thesis: x in W .vertices() reconsider lenW = len W as odd Element of NAT ;

assume x in W .vertices() ; :: thesis: x in (W .reverse()) .vertices()

then consider n being odd Element of NAT such that

A1: n <= len W and

A2: W . n = x by Lm45;

A3: (lenW - n) + 1 is odd Element of NAT by A1, FINSEQ_5:1;

1 <= n by ABIAN:12;

then A4: n in dom W by A1, FINSEQ_3:25;

then n in Seg (len W) by FINSEQ_1:def 3;

then (lenW - n) + 1 in Seg (len W) by FINSEQ_5:2;

then (lenW - n) + 1 in dom W by FINSEQ_1:def 3;

then (lenW - n) + 1 <= len W by FINSEQ_3:25;

then A5: (lenW - n) + 1 <= len (W .reverse()) by FINSEQ_5:def 3;

(W .reverse()) . (((len W) - n) + 1) = x by A2, A4, Th23;

hence x in (W .reverse()) .vertices() by A3, A5, Lm45; :: thesis: verum

end;assume x in W .vertices() ; :: thesis: x in (W .reverse()) .vertices()

then consider n being odd Element of NAT such that

A1: n <= len W and

A2: W . n = x by Lm45;

A3: (lenW - n) + 1 is odd Element of NAT by A1, FINSEQ_5:1;

1 <= n by ABIAN:12;

then A4: n in dom W by A1, FINSEQ_3:25;

then n in Seg (len W) by FINSEQ_1:def 3;

then (lenW - n) + 1 in Seg (len W) by FINSEQ_5:2;

then (lenW - n) + 1 in dom W by FINSEQ_1:def 3;

then (lenW - n) + 1 <= len W by FINSEQ_3:25;

then A5: (lenW - n) + 1 <= len (W .reverse()) by FINSEQ_5:def 3;

(W .reverse()) . (((len W) - n) + 1) = x by A2, A4, Th23;

hence x in (W .reverse()) .vertices() by A3, A5, Lm45; :: thesis: verum

then consider n being odd Element of NAT such that

A6: n <= len (W .reverse()) and

A7: (W .reverse()) . n = x by Lm45;

A8: 1 <= n by ABIAN:12;

then n in dom (W .reverse()) by A6, FINSEQ_3:25;

then A9: W . (((len W) - n) + 1) = x by A7, FINSEQ_5:def 3;

A10: n <= len W by A6, FINSEQ_5:def 3;

then n in Seg (len W) by A8, FINSEQ_1:1;

then (lenW - n) + 1 in Seg (len W) by FINSEQ_5:2;

then A11: (lenW - n) + 1 <= len W by FINSEQ_1:1;

(lenW - n) + 1 is odd Element of NAT by A10, FINSEQ_5:1;

hence x in W .vertices() by A9, A11, Lm45; :: thesis: verum