let G be _Graph; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( W .reverse() is_Walk_from y,x implies W is_Walk_from x,y )
assume A2: W .reverse() is_Walk_from y,x ; :: thesis: 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; :: thesis: verum