theorem :: GLIB_001:148

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