theorem :: GLIB_001:138

for G being _Graph
for W being Walk of G holds
( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n ) by Lm57;