theorem :: GLIBPRE1:26

for G being _Graph
for P being Path of G holds P .length() c= G .order()