:: deftheorem defines is_Walk_from GLIB_001:def 23 :
for G being _Graph
for u, v being object
for W being Walk of G holds
( W is_Walk_from u,v iff ( W .first() = u & W .last() = v ) );