for G being _Graph
for W1 being Trail of G st W1 is V5() holds
ex W2 being Path of W1 st W2 is V5()