theorem :: GLIBPRE1:33

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 holds
( len W1 <= len W2 iff W1 .length() <= W2 .length() )