:: deftheorem defines .last() GLIB_001:def 7 :
for G being _Graph
for W being Walk of G holds W .last() = W . (len W);