theorem :: GLIB_001:84

for G being _Graph
for W being Walk of G holds (W .reverse()) .edgeSeq() = Rev (W .edgeSeq())