theorem :: GLIB_001:97

for G being _Graph
for W being Walk of G
for x, y being set st x in W .vertices() & y in W .vertices() holds
ex W9 being Walk of G st W9 is_Walk_from x,y