theorem Th81: :: GLIB_001:83

for G being _Graph
for e, x, y being object holds
( e Joins x,y,G iff (G .walkOf (x,e,y)) .edgeSeq() = <*e*> )