for G being _Graph
for e, x, y being object st e Joins x,y,G holds
( (G .walkOf (x,e,y)) .first() = x & (G .walkOf (x,e,y)) .last() = y & G .walkOf (x,e,y) is_Walk_from x,y )