theorem :: GLIB_001:128

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