for G being _Graph
for W being Walk of G holds
( W is V5() iff ex v being Vertex of G st W = G .walkOf v ) by Lm56;