theorem :: GLIB_001:90

for G being _Graph
for v being Vertex of G holds (G .walkOf v) .vertices() = {v}