theorem :: GLIBPRE1:27

for G being _Graph
for T being Trail of G holds T .length() c= G .size()