let G be _Graph; :: thesis: for W being Walk of G holds W .edges() = () .edges()
let W be Walk of G; :: thesis:
now :: thesis: for e being object holds
( ( e in W .edges() implies e in () .edges() ) & ( e in () .edges() implies e in W .edges() ) )
let e be object ; :: thesis: ( ( e in W .edges() implies e in () .edges() ) & ( e in () .edges() implies e in W .edges() ) )
hereby :: thesis: ( e in () .edges() implies e in W .edges() )
assume e in W .edges() ; :: thesis: e in () .edges()
then consider n being even Element of NAT such that
A1: 1 <= n and
A2: n <= len W and
A3: W . n = e by Lm46;
A4: n in dom W by ;
then A5: ((len W) - n) + 1 in dom () by Th23;
then reconsider rn = ((len W) - n) + 1 as even Element of NAT ;
A6: 1 <= rn by ;
A7: rn <= len () by ;
e = () . (((len W) - n) + 1) by A3, A4, Th23;
hence e in () .edges() by A6, A7, Lm46; :: thesis: verum
end;
assume e in () .edges() ; :: thesis:
then consider n being even Element of NAT such that
A8: 1 <= n and
A9: n <= len () and
A10: (W .reverse()) . n = e by Lm46;
A11: n in dom () by ;
then A12: ((len ()) - n) + 1 in dom () by Th23;
then reconsider rn = ((len ()) - n) + 1 as even Element of NAT ;
e = () . (((len ()) - n) + 1) by ;
then A13: e = W . rn ;
rn in dom W by A12;
then A14: rn <= len W by FINSEQ_3:25;
1 <= rn by ;
hence e in W .edges() by ; :: thesis: verum
end;
hence W .edges() = () .edges() by TARSKI:2; :: thesis: verum