let G be _Graph; :: thesis: for W being Walk of G holds W .vertices() = () .vertices()
let W be Walk of G; :: thesis:
now :: thesis: for x being object holds
( ( x in W .vertices() implies x in () .vertices() ) & ( x in () .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 () .vertices() ) & ( x in () .vertices() implies x in W .vertices() ) )
hereby :: thesis: ( x in () .vertices() implies x in W .vertices() )
reconsider lenW = len W as odd Element of NAT ;
assume x in W .vertices() ; :: thesis:
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 ;
1 <= n by ABIAN:12;
then A4: n in dom W by ;
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 () by FINSEQ_5:def 3;
(W .reverse()) . (((len W) - n) + 1) = x by A2, A4, Th23;
hence x in () .vertices() by A3, A5, Lm45; :: thesis: verum
end;
assume x in () .vertices() ; :: thesis:
then consider n being odd Element of NAT such that
A6: n <= len () and
A7: (W .reverse()) . n = x by Lm45;
A8: 1 <= n by ABIAN:12;
then n in dom () by ;
then A9: W . (((len W) - n) + 1) = x by ;
A10: n <= len W by ;
then n in Seg (len W) by ;
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 ;
hence x in W .vertices() by ; :: thesis: verum
end;
hence W .vertices() = () .vertices() by TARSKI:2; :: thesis: verum