theorem Th86: :: GLIB_001:88

for G being _Graph
for W being Walk of G holds
( W .first() in W .vertices() & W .last() in W .vertices() )