theorem Th21: :: GLIB_001:22

for G being _Graph
for W being Walk of G holds
( W .first() = (W .reverse()) .last() & W .last() = (W .reverse()) .first() )