theorem :: GLIB_001:140

for G being _Graph
for W being Walk of G holds
( W is Trail-like iff W .reverse() is Trail-like ) by Lm58;