theorem :: GLIB_001:144

for G being _finite _Graph
for W being Trail of G holds len (W .edgeSeq()) <= G .size()