:: deftheorem Def5 defines .walkOf GLIB_001:def 5 :
for G being _Graph
for x, y, e being object holds
( ( e Joins x,y,G implies G .walkOf (x,e,y) = <*x,e,y*> ) & ( not e Joins x,y,G implies G .walkOf (x,e,y) = G .walkOf the Element of the_Vertices_of G ) );