theorem Th89: :: GLIB_001:91

for G being _Graph
for e, x, y being object st e Joins x,y,G holds
(G .walkOf (x,e,y)) .vertices() = {x,y}