theorem :: GLIB_001:18

for G being _Graph
for W being Walk of G
for x, y being object st W is_Walk_from x,y holds
( x is Vertex of G & y is Vertex of G ) ;