theorem :: GLIB_001:166

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