theorem Th25: :: GLIB_009:25

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