theorem :: GLIB_001:166

for G being _Graph
for W1 being Trail of G st not W1 is trivial holds
ex W2 being Path of W1 st not W2 is trivial