theorem Th15: :: GLIB_007:15

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W1 being Walk of G1 holds W1 is Walk of G2