let G be _Graph; :: thesis: for W being Walk of G
for x, y being set 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 set holds
( W is_Walk_from x,y iff W .reverse() is_Walk_from y,x )
let x, y be set ; :: 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;

hereby :: thesis: ( W .reverse() is_Walk_from y,x implies W is_Walk_from x,y )

assume A2: W is_Walk_from x,y ; :: thesis: W .reverse() is_Walk_from y,x
then W . (len W) = y by Th18;
then A3: (W .reverse()) . 1 = y by FINSEQ_5:62;
W . 1 = x by A2, Th18;
then (W .reverse()) . (len W) = x by FINSEQ_5:62;
hence W .reverse() is_Walk_from y,x by A1, A3, Th18; :: thesis: verum

end;

assume A4: W .reverse() is_Walk_from y,x ; :: thesis: W is_Walk_from x,y
then (W .reverse()) . 1 = y by Th18;
then A5: W . (len W) = y by FINSEQ_5:62;
(W .reverse()) . (len (W .reverse())) = x by A4, Th18;
then W . 1 = x by A1, FINSEQ_5:62;
hence W is_Walk_from x,y by A5, Th18; :: thesis: verum