theorem Th80: :: GLIB_006:76

for G2 being _Graph
for G1 being Supergraph of G2
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) & ( W1 is Cycle-like implies W2 is Cycle-like ) & ( W2 is Cycle-like implies W1 is Cycle-like ) )