:: deftheorem defines .first() GLIB_001:def 6 :
for G being _Graph
for W being Walk of G holds W .first() = W . 1;