for G being _Graph
for W being Walk of G st W is open & W is Path-like holds
W is vertex-distinct