let G be _Graph; for W being Walk of G
for x, y being object holds
( W is_Walk_from x,y iff W .reverse() is_Walk_from y,x )
let W be Walk of G; for x, y being object holds
( W is_Walk_from x,y iff W .reverse() is_Walk_from y,x )
let x, y be object ; ( W is_Walk_from x,y iff W .reverse() is_Walk_from y,x )
A1:
len W = len (W .reverse())
by FINSEQ_5:def 3;
thus
( W is_Walk_from x,y implies W .reverse() is_Walk_from y,x )
by A1, FINSEQ_5:62; ( W .reverse() is_Walk_from y,x implies W is_Walk_from x,y )
assume A2:
W .reverse() is_Walk_from y,x
; W is_Walk_from x,y
then
(W .reverse()) . 1 = y
;
then A3:
W . (len W) = y
by FINSEQ_5:62;
(W .reverse()) . (len (W .reverse())) = x
by A2;
then
W . 1 = x
by A1, FINSEQ_5:62;
hence
W is_Walk_from x,y
by A3; verum