theorem Th132: :: GLIB_001:134

for G being _Graph
for W1, W2 being Walk of G st W2 is trivial & W2 .edges() c= W1 .edges() holds
W2 .vertices() c= W1 .vertices()