:: deftheorem defines .length() GLIB_001:def 18 :
for G being _Graph
for W being Walk of G holds W .length() = len (W .edgeSeq());