theorem Th16: :: GLIB_007:16

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds
( W1 is directed iff W2 .reverse() is directed )