theorem Th173: :: GLIB_001:175

for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G2 holds
( ( W is closed implies W is closed Walk of G1 ) & ( W is directed implies W is directed Walk of G1 ) & ( W is trivial implies W is trivial Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )